UpperHeadSharpFrozenAbsorption

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Frozen-scale comparison for the sharp wave-head carrier

This file performs terminal numerical comparisons for the sharp wave-head carrier, both locally at one strict descendant and after the root-plus-depth assembly. It retains the ordinary factor cstar⁻¹ * s * gamma * (2 * s - gamma)⁻³ and absorbs the rare carrier at the frozen exceptional scale. The endpoint s = 1 is stated explicitly.

These are internal Provider estimates. They do not alter a frozen declaration and carry no source-node or closure status.

Direct tuned collar-head trace

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.collarHeadTunedPerDescendantOutputConst (d : ℕ) : ℝ

One dimension-only gate for the direct tuned collar-head trace. It pays both the profile auxiliary threshold and the tuned trace absorption.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.collar_head_tuned_trace_is_big_o_with_eighth_power {d : ℕ} (M : ABKModel d) {m : ℤ} {k : ℕ} {R : HCPolySupport.TriadicCube d} (hR : R ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d m) (m - 1 - ↑k)) {E : { E : ℝ // 1 ≤ E }} (hS : Frozen.Section3.inductionState M (m - 1) E) {sigma Cup : ℝ} (hsigma0 : 0 < sigma) (hsigma : sigma ≤ 1 / 2) (hmax : max (Real.exp (Cup / sigma)) (Disorder.cstar M)⁻¹ ≤ ↑E) (hEgamma : ↑E ≤ M.gamma ^ (-(1 / 5))) (houtput : collarHeadTunedPerDescendantOutputConst d ≤ Cup) : have trace := fun (omega : Cutoff.CutoffSample d) => ∑ j : Fin d, ∑' (n : ℕ), Multiscale.probeSharpFramedCollarWavePart M R.scale (↑E) bfaProfileB (collarBandMeanDepth M ↑E) n (m - 1) (HCPolySupport.basisVec j) (Affine.superposedGradConst d) (fun (eta : Cutoff.CutoffSample d) => Multiscale.waveHeadTerm M R.scale (↑E) bfaProfileB (probeSharpLayerAnchor R.scale bfaProfileB (collarBandMeanDepth M ↑E) n) eta ^ 2) (Cutoff.translateCutoffSample (HCPolySupport.triadicCubeShift R) omega); (∀ (omega : Cutoff.CutoffSample d), 0 ≤ trace omega) ∧ Measurable trace ∧ (∀ᵐ (omega : Cutoff.CutoffSample d) ∂↑(Cutoff.cutoffSampleLaw M), ENNReal.ofReal (trace omega) = ∑ j : Fin d, ∑' (n : ℕ), ENNReal.ofReal (Multiscale.probeSharpFramedCollarWavePart M R.scale (↑E) bfaProfileB (collarBandMeanDepth M ↑E) n (m - 1) (HCPolySupport.basisVec j) (Affine.superposedGradConst d) (fun (eta : Cutoff.CutoffSample d) => Multiscale.waveHeadTerm M R.scale (↑E) bfaProfileB (probeSharpLayerAnchor R.scale bfaProfileB (collarBandMeanDepth M ↑E) n) eta ^ 2) (Cutoff.translateCutoffSample (HCPolySupport.triadicCubeShift R) omega))) ∧ HCPolySupport.IndependentSums.IsBigOWith (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma ((1 - sigma) / 3)) trace (3 ^ (M.gamma * (↑k + 1)) * Real.exp (-(Cup⁻¹ * ((↑E)⁻¹ ^ 2 * M.gamma⁻¹))) ^ 8)

The literal finite-coordinate collar-head trace at the common tuned depth has the eighth-power local rare scale required by the per-descendant upper assembly. No root, grid, or depth wrapper intervenes.