UpperWaveTailTraceE12Consumption

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

Exact consumption for the strict-descendant wave-tail trace

This file forms the finite-coordinate trace of the literal named framed wave-tail Whitney lane at one strict descendant. The coordinatewise comparison is intersected over the finite basis and summed, yielding the exact bounded-plus-rare real trace carriers at the translated descendant sample.

The final declaration also prices the literal collar wave-tail summand at the common collar/band-mean depth, directly from the induction state and frozen gates. The descendant maximum, positive-depth aggregation, root row, other named lanes, complete envelope, cutoff observable, and all-exponent estimate remain outside this file. These declarations are conditional internal Provider A and carry no source-node, source-node-instance, fractional-node, or closure status.

Direct common-depth collar wave-tail terminal

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

Dimension-only output threshold for the literal collar copy of the common-depth squared wave tail. The displayed coefficient is exactly the finite-coordinate Whitney-sum prefactor used in the proof below; the leading 1 makes its nonnegativity explicit.

Equations

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

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.isBigOWith_upperProfileTarget_collarWaveTailFiniteTrace {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 : probeSharpCollarWaveTailTunedOutputConst 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.waveTailTerm M R.scale (↑E) bfaProfileB R.scale (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.waveTailTerm M R.scale (↑E) bfaProfileB R.scale (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 named summand 12, summed over the common-depth Whitney family and the finite coordinate basis, has the frozen upper-profile bound at the exact terminal scale. Summability and measurability are derived internally.