LambdaSlotConsumer

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

Bullet (B5) at the λ-slot that Step 3's display actually reads

The carrier gap this module closes

MajorantSlots.step3DisplayAt reads its λ-slot as

( unitCubeLambda (2γ) 2 ( unitRescaledCutoffCoeff M R (R.scale − 2) ω ) )^{-1} ,

the frozen Section-2.4 unit-cube gauge of the rescaled cutoff object at the gapped gauge s = 2γ, whereas LambdaIndexUpscale.lambdaPrintedAtom is the manuscript's λ_{γ,2}^{-1}(z + □_j; 𝐚_{j−2}) at the printed gauge γ. Two proved identities and one antitonicity close the gap at constant 1:

1. BadEvents.unitCubeLambda_unitRescaledCutoffCoeff — the unit-cube gauge of the rescaled object IS Ch02.lambdaSq R s q (𝐚_{R.scale−2});
2. Localize.inv_lambdaSq_two_antitone_gauge — λ^{-1} is antitone in the gauge, so the γ-reading dominates the 2γ-reading (this is the ONE available direction, and here it is the useful one);
3. BadEvents.cubeLowerEllipticityInvLiteral_translateCutoffSample together with BadEvents.cubeLowerEllipticityInvLiteral_inv_eq_lambdaSq — the cube R at the field 𝐚_{R.scale−2} is the origin cube □_{R.scale} at the sample translated by R's base point, which is exactly lambdaPrintedAtom M R.scale (triadicCubeShift R).

Consequently the whole (B5) moment bound of LambdaIndexUpscale — printed cube □_j, printed field 𝐚_{j−2}, printed gauge σ_{j−1}, constant 64(1+9^d) — transfers verbatim to the slot Step 3 consumes. No γ-exponent and no s-power is moved.

References

• ABK26, l.bounds.mathcal.E.aL bullet (B5); Step 3 display e.apply.sensitivity.J.aL.

1. The pointwise carrier bridge

theorem Algsuperdiff.Section4.Provider.BoundsEaL.inv_unitCubeLambda_twoGamma_le_lambdaPrintedAtom {d : ℕ} (M : Section3.ABKModel d) (R : HCPolySupport.TriadicCube d) (omega : Section3.Cutoff.CutoffSample d) : (Frozen.Section24.unitCubeLambda (2 * M.gamma) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) (Section3.Provider.BadEvents.unitRescaledCutoffCoeff M R (R.scale - 2) omega))⁻¹ ≤ lambdaPrintedAtom M R.scale (HCPolySupport.triadicCubeShift R) omega

The λ-slot of Step 3's display is dominated by the printed (B5) atom.

(unitCubeLambda (2γ) 2 (unitRescaledCutoffCoeff M R (R.scale−2) ω))^{-1} ≤ λ_{γ,2}^{-1}(3^{R.scale}v + □_{R.scale}; 𝐚_{R.scale−2}),

at constant 1. The inequality (rather than equality) is exactly the gauge antitonicity 2γ ≥ γ; the converse is NOT available (A9).

2. The moment bound at the consumed slot

theorem Algsuperdiff.Section4.Provider.BoundsEaL.exists_lintegral_rpow_inv_unitCubeLambda_twoGamma_le (d : ℕ) : ∃ (C : ℝ), 6 ≤ C ∧ ∀ (M : Section3.ABKModel d), M.gamma ≤ C⁻¹ ^ 10 * Section3.Disorder.cstar M ^ 10 → ∃ (E : { E : ℝ // 1 ≤ E }), ↑E = C * (Section3.Disorder.cstar M)⁻¹ ∧ ∀ (R : HCPolySupport.TriadicCube d) (p : ℝ), 1 ≤ p → ∫⁻ (omega : Section3.Cutoff.CutoffSample d), ENNReal.ofReal (Frozen.Section24.unitCubeLambda (2 * M.gamma) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) (Section3.Provider.BadEvents.unitRescaledCutoffCoeff M R (R.scale - 2) omega))⁻¹ ^ p ∂↑(Section3.Cutoff.cutoffSampleLaw M) ≤ ENNReal.ofReal (lambdaUpscaleConst d * ((↑(Section3.Annealed.sigmaBar M (R.scale - 1)))⁻¹ * Support.cgEllipLowerConstant d) + gammaMomentBound (1 / 3) p (lambdaUpscaleConst d * lambdaMaxOrliczConst d * ((↑(Section3.Annealed.sigmaBar M (R.scale - 1)))⁻¹ * Proportion.cgTailScale M ↑E))) ^ p

The consumed-slot bullet, packaged and unconditional in the printed regime. The counterpart of LambdaIndexUpscale.exists_lintegral_rpow_lambdaPrintedAtom_le at the slot Step 3 reads.