Documentation

LeanPool.Superdiffusion.Algsuperdiff.Section4.Provider.Regularity.StepSevenLambdaGoodEvent

StepSevenLambdaGoodEvent #

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

t.regularity Step 7b, clause (B): the good-event ellipticity caps at s* = 1/16 #

The target #

  λ_{1/16,q}^{-1}(z+□_{k'}; 𝐚_{L,k'}) · 1_{𝒢(k',z; s/8, sδ^{1/2}/8)} ≤ C(d) σ_{k'}^{-1} ,
  Λ_{1/16,q}(z+□_{k'}; 𝐚_{L,k'}) · 1_{𝒢(k',z; s/8, sδ^{1/2}/8)}      ≤ C(d) σ_{k'} .

The good-event derivation: clause (B) is unconditional #

ae_stepSevenLambdaCaps below derives all four legs, a.e. on the §4.4 good event itself, from the proved cap ExcessDecay.ae_boundLambdasByEs, whose own source is the frozen theorem Algsuperdiff.Frozen.Section4.annular_decomposition (clause (ii)). Three alignments make it work, and each is exact rather than approximate:

  1. Taking m:= k', t:= ⟨s/8⟩ and ep:= (s/8)δ^{1/2} is a literal match — no ε-monotonicity step and no slot comparison is needed.
  2. The index. The cap proves at the good-event slot s/8 = 1/32 and at q = 2. The q = 2 legs at s* come from index monotonicity (Ch02.LambdaSq_antitone, Ch02.lambdaSq_mono), which runs the right way: 1/32 < 1/16, and a cap at a smaller index is stronger.

The residual conditions, and why none of them is a new obligation #

ae_stepSevenLambdaCaps carries exactly the proved cap's own binders: the annular standing regime γ ≤ C⁻¹c⋆^{10}, the slot floor 8γ ≤ s/8, the δ-range δ ∈ (0,1/2] (which produces the cap's ep ∈ (0,1/2] through stepOneEp_mem_Ioc), and the smallness γ|log γ|² ≤ (s/8)^{3/2} c⋆² · (s/8)δ^{1/2}. These are the §4.4 parameter regime, present verbatim in every proved cap of the development; nothing mathematical is supplied by the caller.

References #

1. Clause (B) as a named record #

source
structure Algsuperdiff.Section4.Provider.Regularity.StepSevenLambdaCaps {d : ℕ} (Q : HCPolySupport.TriadicCube d) (a : HCPolySupport.Book.Ch03.CoeffFamily d) (sigma CB : ℝ) :
Prop

Clause (B): the good-event ellipticity caps at the single index s* = 1/16, both q ∈ {1, 2}, against one comparator sigma (= σ_{k'}) and one constant (= C(d)).

Instances For

    2. The index arithmetic of the re-specification #

    source
    theorem Algsuperdiff.Section4.Provider.Regularity.stepSevenStabilityIndex_div_two :
    stepSevenStabilityIndex / 2 = stepOneSEighth

    The ruled index is exactly twice the good-event slot: s*/2 = s/8. This is what makes CoarseGraining's q = 1 ← q = 2 bridge land on the cap without loss.

    source
    theorem Algsuperdiff.Section4.Provider.Regularity.stepOneSEighth_lt_stepSevenStabilityIndex :
    stepOneSEighth < stepSevenStabilityIndex

    s/8 < s*: the good-event slot sits strictly below the ruled index, so index monotonicity carries the q = 2 cap upward for free.

    3. The comparator algebra #

    4. Clause (B) from a q = 2 ratio cap at the good-event slot #

    source
    theorem Algsuperdiff.Section4.Provider.Regularity.stepSevenLambdaCaps_of_ratio_cap {d : ℕ} [NeZero d] (Q : HCPolySupport.TriadicCube d) (a : HCPolySupport.Book.Ch03.CoeffFamily d) {sigma K : ℝ} (hsigma : 0 < sigma) (hup : sigma⁻¹ * HCPolySupport.Book.Ch02.LambdaSq Q stepOneSEighth (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a ≤ K) (hlo : sigma * (HCPolySupport.Book.Ch02.lambdaSq Q stepOneSEighth (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a)⁻¹ ≤ K) :
    StepSevenLambdaCaps Q a sigma K

    The deterministic core of the Unit-C derivation. A q = 2 ratio cap at the good-event slot s/8 = s*/2 yields clause (B) at s* for BOTH q:

    • q = 2 by index monotonicity (1/32 < 1/16, and λ^{-1}, Λ are nonincreasing in the index);
    • q = 1 by CoarseGraining's q = 1 ← q = 2 bridge at NO constant, which needs the q = 2 datum at exactly half the index — which is exactly the slot.
    source
    theorem Algsuperdiff.Section4.Provider.Regularity.ae_stepSevenLambdaCaps (d : ℕ) [NeZero d] :
    ∃ (C : ℝ), 0 < C ∧ ∀ (M : Section3.ABKModel d), M.gamma ≤ C⁻¹ * Section3.Disorder.cstar M ^ 10 → ∀ delta ∈ Set.Ioc 0 (1 / 2), 8 * M.gamma ≤ stepOneSEighth → M.gamma * |Real.log M.gamma| ^ 2 ≤ stepOneSEighth.rpow (3 / 2) * Section3.Disorder.cstar M ^ 2 * stepOneEp delta → ∀ (k : ℤ) (z : HCPolySupport.Vec d), ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), omega ∈ stepThreeGoodEvent M delta k z → ∀ (L : ℤ), k ≤ L → StepSevenLambdaCaps (HCPolySupport.originCube d k) (Support.fluxCorrectedCoeffFamily M L k (HCPolySupport.originCube d k) (Section3.Cutoff.translateCutoffSample z omega)) (↑(Section3.Annealed.sigmaBar M k)) (2 * ↑d * ((C * stepOneEp delta) ^ 2 + 1))

    Almost surely, on the §4.4 Step-3/Step-7 good event 𝒢(k, z; s/8, (s/8)δ^{1/2}) and for every L ≥ k, the coarse-grained ellipticity constants of the flux-corrected field on □_k satisfy the clause-(B) caps at the index s* = 1/16 and both q ∈ {1,2}, against σ_k and the pure dimensional constant 2d((C·(s/8)δ^{1/2})² + 1).