UpperWaveTailE12Consumption

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

Exact consumption for the translated framed wave-tail lane

This file connects the bounded and rare witnesses to the literal named good-cell wave-tail summand in the framed descendant envelope. The comparison uses the exact descendant scale and translated cutoff sample. Almost-everywhere summability is derived from the existing layerwise Gamma estimates, so no summability assertion is added as a caller obligation when the real layer sums are identified with the literal envelope.

Only one named good-cell wave-tail lane and one basis coordinate are consumed. The root row, collar wave-tail lane, eleven other named lanes, complete framed envelope, cutoff observable, and upper-leg export are not treated here.

The literal lane at the common Section 3 depth

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

The positive rate left by the squared wave-tail gain when its anchor uses the common collar/band-mean depth.

Equations

• Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpWaveTailTunedRate d = ↑d / 4 * Real.log 3 * Algsuperdiff.Section3.Provider.CoarseEllipticity.collarBandMeanDepthCoeff d

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpWaveTailTunedOffset {d : ℕ} (M : ABKModel d) (E : ℝ) (k n : ℕ) : ℝ

The deterministic descendant offset removed before applying the hsep split at the common depth.

Equations

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

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpWaveTailTunedBaseTerm {d : ℕ} (M : ABKModel d) (root : ℤ) (E : ℝ) (k n : ℕ) (omega : Cutoff.CutoffSample d) : ℝ

The unframed squared wave-tail carrier at the common depth.

Equations

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

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpWaveTailTunedBaseScale {d : ℕ} (M : ABKModel d) (root : ℤ) (E sigma : ℝ) (k n : ℕ) : ℝ

The exact profile-tail scale of the common-depth unframed carrier.

Equations

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

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpWaveTailTunedBoundedLayer {d : ℕ} (M : ABKModel d) (root : ℤ) (E : ℝ) (k n : ℕ) (omega : Cutoff.CutoffSample d) : ℝ

The bounded-hsep witness at the common depth.

Equations

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

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpWaveTailTunedRareLayer {d : ℕ} (M : ABKModel d) (root : ℤ) (E : ℝ) (k n : ℕ) (omega : Cutoff.CutoffSample d) : ℝ

The residual-hsep witness at the common depth.

Equations

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

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpWaveTailTunedBoundedLayerScale {d : ℕ} (M : ABKModel d) (root : ℤ) (E sigma : ℝ) (k n : ℕ) : ℝ

The doubled base stochastic scale for a bounded wave-tail layer.

Equations

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

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpWaveTailTunedRareLayerScale {d : ℕ} (M : ABKModel d) (root : ℤ) (E sigma : ℝ) (k n : ℕ) : ℝ

The product-tail stochastic scale for a rare wave-tail layer.

Equations

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

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpWaveTailTunedBoundedLayerBound {d : ℕ} (M : ABKModel d) (E sigma : ℝ) (n : ℕ) : ℝ

The deterministic geometric budget for a bounded wave-tail layer.

Equations

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

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpWaveTailTunedRareLayerBound {d : ℕ} (M : ABKModel d) (E sigma : ℝ) (n : ℕ) : ℝ

The deterministic geometric budget for a rare wave-tail layer.

Equations

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

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

A common constant for the bounded and rare wave-tail trace sums.

Equations

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

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpWaveTailTunedTraceScale {d : ℕ} (M : ABKModel d) (E sigma : ℝ) : ℝ

The stochastic scale for the full tuned wave-tail trace.

Equations

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

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

The prefactor obtained by absorbing the wave-tail trace's exponential decay.

Equations

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

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

A common output constant for the tuned wave-tail bounds.

Equations

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

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.exists_good_wave_tail_tuned_finite_trace_split {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 }} (hstate : 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 : probeSharpWaveTailTunedOutputConst d ≤ Cup) : ∃ (bounded : Cutoff.CutoffSample d → ℝ) (rare : Cutoff.CutoffSample d → ℝ), (∀ (omega : Cutoff.CutoffSample d), 0 ≤ bounded omega) ∧ Measurable bounded ∧ (∀ (omega : Cutoff.CutoffSample d), 0 ≤ rare omega) ∧ Measurable rare ∧ (∀ᵐ (omega : Cutoff.CutoffSample d) ∂↑(Cutoff.cutoffSampleLaw M), ∑ j : Fin d, ∑' (n : ℕ), Multiscale.probeSharpFramedGoodWavePart M R.scale (↑E) bfaProfileB (collarBandMeanDepth M ↑E) n (m - 1) (HCPolySupport.basisVec j) (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) ≤ bounded omega + rare omega) ∧ (∀ᵐ (omega : Cutoff.CutoffSample d) ∂↑(Cutoff.cutoffSampleLaw M), ∑ j : Fin d, ∑' (n : ℕ), ENNReal.ofReal (Multiscale.probeSharpFramedGoodWavePart M R.scale (↑E) bfaProfileB (collarBandMeanDepth M ↑E) n (m - 1) (HCPolySupport.basisVec j) (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)) = ENNReal.ofReal (∑ j : Fin d, ∑' (n : ℕ), Multiscale.probeSharpFramedGoodWavePart M R.scale (↑E) bfaProfileB (collarBandMeanDepth M ↑E) n (m - 1) (HCPolySupport.basisVec j) (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) ∂↑(Cutoff.cutoffSampleLaw M), ∑ j : Fin d, ∑' (n : ℕ), ENNReal.ofReal (Multiscale.probeSharpFramedGoodWavePart M R.scale (↑E) bfaProfileB (collarBandMeanDepth M ↑E) n (m - 1) (HCPolySupport.basisVec j) (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)) ≤ ENNReal.ofReal (bounded omega) + ENNReal.ofReal (rare omega)) ∧ HCPolySupport.IndependentSums.IsBigOWith (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma ((1 - sigma) / 3)) bounded (probeSharpWaveTailTunedTraceScale M (↑E) sigma) ∧ HCPolySupport.IndependentSums.IsBigOWith (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma ((1 - sigma) / 3)) rare (probeSharpWaveTailTunedTraceScale M (↑E) sigma) ∧ 0 ≤ probeSharpWaveTailTunedTraceScale M (↑E) sigma ∧ probeSharpWaveTailTunedTraceScale M (↑E) sigma ≤ Real.exp (-(Cup⁻¹ * ((↑E)⁻¹ ^ 2 * M.gamma⁻¹))) ^ 8