StepFourFinalIteration

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

hstep4, discharged on the interior branch

What this module is

StepFiveIterationResult.iterationDecay_of_stepFourDecay takes one mathematical input, hstep4. This module produces it on the interior branch, from the frozen statements and the supply events alone:

   ∀ j ∈ [n+k, m-1] ∖ 𝓑_z ,
     E(u, U_{j-k}) ≤ θ^k E(u, U_j) + C_ε ε_j(z,ω) |∇ℓ_j| + δ_j ,
   U_j = stepThreeWindow z m j ,  θ = 3^{-1/4} ,
   δ_j = C_δ 3^{j/2} σ_j^{-1} ( K_g C_{S4.4}(d,s) ) .

ε_j is StepFiveBudgetSums.stepFiveEps — the Step-5 slot itself, at the unshifted index j (the interior clause reads its event and its flux representative at the printed index), carrying the coefficient C_ε = edFinalEpsCoeff. δ_j is the g-leg of the Step-5 family at the root's own Hölder datum K_g: there is no ∇h leg and no boundary indicator, so the ungated non-decaying flat leg does not arise either.

The three pins

• s := 1/4 (stepOneS). At that value the excess-decay supply event 𝒢(j, z; s/8, (s/8)√δ) and the Step-3/Step-1 good event 𝒢(j, z; s/8, ε(δ)) are the same term — event_pin is rfl. It is also what makes γ ≤ 1/256 deliver the excess-decay binder s ∈ [64γ, 1] and s < 1/2 deliver the Gagliardo index range.
• the bad set is StepThreeBadSet.stepThreeBadSet verbatim: j ∉ 𝓑_z with n ≤ j ≤ m-1 is the supply event at j.
• the δ-gate (hgate) is the absorption inequality at the annular cap ε_j ≤ C_ann ε(δ): an explicit hypothesis on (k, δ), and the inequality δ is chosen to satisfy after k. It is a hypothesis, not a smuggled fact.

References

• ABK26, t.regularity Steps 1--5; l.excess.decay.good.scales.

1. The composed per-scale display

theorem Algsuperdiff.Section4.Provider.Regularity.stepFourDecay_interior_of_anchors (d : ℕ) [NeZero d] (hd : d ≠ 0) : ∃ (C : ℝ), 0 < C ∧ ∃ (k₀ : ℕ), 3 ≤ k₀ ∧ ∀ (k : ℕ), k₀ ≤ k → ∀ (M : Section3.ABKModel d) (m0 : ℤ) (Ecap : { E : ℝ // 1 ≤ E }), Frozen.Section3.inductionState M m0 Ecap → M.gamma ≤ 1 / 4 → ∀ s ∈ Set.Icc (64 * M.gamma) 1, s < 1 / 2 → M.gamma ≤ C⁻¹ * Section3.Disorder.cstar M ^ 10 → M.gamma * |Real.log M.gamma| ^ 2 ≤ (s / 8).rpow (3 / 2) * Section3.Disorder.cstar M ^ 2 * (C⁻¹ * s ^ 4) → ∀ (hs : 0 < s), ∀ delta ≤ 1, ∀ (L m : ℤ), m ≤ L → m ≤ m0 → ∀ z ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d (m - 1)), ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), ∀ (n : ℤ), n + 1 ≤ m → omega ∈ Frozen.Section4.goodEventAt M (Support.cgEllipLowerConstant d) n z ⟨s / 8, ⋯⟩ (s / 8 * √delta) → ∀ (u hdat : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) (g : HCPolySupport.Vec d → HCPolySupport.Vec d), Support.IsDirichletSolutionOn (Section3.Cutoff.coefficientCutoff M.nu L omega).toCoeffField (HCPolySupport.originCube d m) u hdat g → MeasureTheory.MemLp g 2 (Support.normalizedVolumeMeasureOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) → MeasureTheory.MemLp (HCPolySupport.Gagliardo.gagliardoKernel s 2 g) 2 (Support.normalizedGagliardoMeasureOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) → MeasureTheory.MemLp (HCPolySupport.Gagliardo.gagliardoKernel s 2 hdat.grad) 2 (Support.normalizedGagliardoMeasureOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) → ∀ (Kg epsj : ℝ), 0 ≤ Kg → 0 ≤ epsj → Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (1 / 2) Kg g → Support.fluxCorrectedErrorRepresentative M L n ⟨s / 8, ⋯⟩ (Section3.Cutoff.translateCutoffSample z omega) ≤ epsj → edFinalEpsCoeff d C k s * epsj ≤ 1 / 2 * 3 ^ (-(1 / 4) * ↑k) → ∀ (c : ℝ) (gmin : HCPolySupport.Vec d), Support.IsAffineMinimizer (stepThreeWindow z m n) u.toFun c gmin → Support.affineExcess (stepThreeWindow z m (n - ↑k)) u.toFun ≤ 3 ^ (-(1 / 4) * ↑k) * Support.affineExcess (stepThreeWindow z m n) u.toFun + edFinalEpsCoeff d C k s * epsj * Support.slopeMagnitude gmin + edFinalDelta M (edFinalDeltaConst d C k s) (Kg * stepFourGagliardoConst d s) n

The Step-4 collapse composed at one scale, on the interior branch.

The two-leg one-step contraction off the anchor's frontier-empty clause, at x := z, with all its carried items discharged from EdFinalInputs (the two gates from z ∈ □_{m-1}, the harmonic replacement pair from u), and the Step-4 collapse applied.

2. The Step-1 pin s = 1/4, and the identification of the two events

theorem Algsuperdiff.Section4.Provider.Regularity.stepOneS_mem_Icc {d : ℕ} {M : Section3.ABKModel d} (hgamma : M.gamma ≤ 1 / 256) : stepOneS ∈ Set.Icc (64 * M.gamma) 1

theorem Algsuperdiff.Section4.Provider.Regularity.stepOneS_lt_half : stepOneS < 1 / 2

3. hstep4, discharged

theorem Algsuperdiff.Section4.Provider.Regularity.stepFourDecay_interior_pinned (d : ℕ) [NeZero d] (hd : d ≠ 0) : ∃ (C : ℝ) (Cann : ℝ), 0 < C ∧ 0 < Cann ∧ ∃ (k₀ : ℕ), 3 ≤ k₀ ∧ ∀ (k : ℕ), k₀ ≤ k → ∀ (M : Section3.ABKModel d) (m0 : ℤ) (Ecap : { E : ℝ // 1 ≤ E }), Frozen.Section3.inductionState M m0 Ecap → M.gamma ≤ C⁻¹ * Section3.Disorder.cstar M ^ 10 → M.gamma ≤ Cann⁻¹ * Section3.Disorder.cstar M ^ 10 → M.gamma ≤ 1 / 256 → M.gamma * |Real.log M.gamma| ^ 2 ≤ (stepOneS / 8).rpow (3 / 2) * Section3.Disorder.cstar M ^ 2 * (C⁻¹ * stepOneS ^ 4) → ∀ delta ∈ Set.Ioc 0 (1 / 2), M.gamma * |Real.log M.gamma| ^ 2 ≤ stepOneSEighth.rpow (3 / 2) * Section3.Disorder.cstar M ^ 2 * stepOneEp delta → edFinalEpsCoeff d C k stepOneS * (Cann * stepOneEp delta) ≤ 1 / 2 * 3 ^ (-(1 / 4) * ↑k) → ∀ (L m : ℤ), m ≤ L → m ≤ m0 → ∀ z ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d (m - 1)), ∀ (n : ℤ), ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), ∀ (u hdat : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) (g : HCPolySupport.Vec d → HCPolySupport.Vec d) (Kg : ℝ), 0 ≤ Kg → Support.IsDirichletSolutionOn (Section3.Cutoff.coefficientCutoff M.nu L omega).toCoeffField (HCPolySupport.originCube d m) u hdat g → MeasureTheory.MemLp g 2 (Support.normalizedVolumeMeasureOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) → MeasureTheory.MemLp (HCPolySupport.Gagliardo.gagliardoKernel stepOneS 2 g) 2 (Support.normalizedGagliardoMeasureOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) → MeasureTheory.MemLp (HCPolySupport.Gagliardo.gagliardoKernel stepOneS 2 hdat.grad) 2 (Support.normalizedGagliardoMeasureOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) → Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (1 / 2) Kg g → ∀ (c : ℤ → ℝ) (slope : ℤ → HCPolySupport.Vec d), (∀ j ≤ m, Support.IsAffineMinimizer (stepThreeWindow z m j) u.toFun (c j) (slope j)) → ∀ (j : ℤ), n + ↑k ≤ j → j ≤ m - 1 → j ∉ stepThreeBadSet M delta n m z omega → Support.affineExcess (stepThreeWindow z m (j - ↑k)) u.toFun ≤ stepFiveTheta ^ k * Support.affineExcess (stepThreeWindow z m j) u.toFun + edFinalEpsCoeff d C k stepOneS * stepFiveEps M j z delta omega * Support.slopeMagnitude (slope j) + edFinalDelta M (edFinalDeltaConst d C k stepOneS) (Kg * stepFourGagliardoConst d stepOneS) j

hstep4 on the interior branch, discharged.

For one omega and every scale j ∈ [n+k, m-1] outside the Step-3 bad set 𝓑_z, the Step-4 per-scale excess decay holds at the concrete windows U_j = stepThreeWindow z m j, the Step-5 slot ε_j (times the collapse's coefficient) and the g-leg δ_j — with NO harmonic-approximation hypothesis, NO ∇h leg, NO boundary indicator, and no conditional beyond the annular producer's own premises and the explicit δ-gate. This is the input of StepFiveIterationResult.iterationDecay_of_stepFourDecay.