StepFourFinalEndpoint

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

e.oscillation.iteration.result with hstep4 GONE

What this module is

StepFiveConcreteEndpoint.stepFiveConcreteOscillationResult_of_stepFourDecay is the Step-5 endpoint with hstep4 as the one conditional input. This module is its interior-branch sibling with hstep4 gone: the Step-4 decay is supplied by StepFourFinalIteration.stepFourDecay_interior_pinned off the frozen statements and the supply events, and the two budgets by StepFourFinalBudget.

• the ε-slot carries the collapse's coefficient C_ε, absorbed by the generic re-run at C_iter = 2C₀(k+1+C_ε);
• the δ-family is the interior g-leg alone, at the root's own Hölder datum K_g rather than the W^{1/2,∞} seminorm it dominates;
• dataH = 0 — the interior clause carries no ∇h leg and no boundary indicator, so the whole 1_{z ∉ □_{m-1}} half of the printed dataH slot is absent. This is the pay-off of gating at z ∈ □_{m-1}: on that half of the lattice the printed indicator is 0 and the interior route reproduces it exactly.

What is NOT in this module

The boundary branch (z ∉ □_{m-1}), where's general-clause route with its ∇h legs's excessDecay_oneStep_anchored join are needed, and where's mismatch (3) (the flat ungated ‖∇h‖_∞ leg with no decay in n) is still open.

References

• ABK26, t.regularity Steps 4--5.

theorem Algsuperdiff.Section4.Provider.Regularity.edFinal_oscillationIterationResult_interior (d : ℕ) [NeZero d] (hd : d ≠ 0) : ∃ (C : ℝ) (Cann : ℝ), 0 < C ∧ 0 < Cann ∧ ∃ (k₀ : ℕ), 3 ≤ k₀ ∧ ∀ (k : ℕ), k₀ ≤ k → 2 ≤ k → ∃ (Cout : ℝ) (Citer : ℝ), 0 < Cout ∧ 0 ≤ Citer ∧ ∀ (M : Section3.ABKModel d) (m0 : ℤ) (Ecap : { E : ℝ // 1 ≤ E }), Frozen.Section3.inductionState M m0 Ecap → M.gamma < 1 / 2 → 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) → ∀ (Cedos Cannp alpha : ℝ), alpha ≤ 1 → stepOneDelta (stepOneC1 d Cedos Cannp Citer k) alpha ∈ Set.Ioc 0 (1 / 2) → M.gamma * |Real.log M.gamma| ^ 2 ≤ stepOneSEighth.rpow (3 / 2) * Section3.Disorder.cstar M ^ 2 * stepOneEp (stepOneDelta (stepOneC1 d Cedos Cannp Citer k) alpha) → edFinalEpsCoeff d C k stepOneS * (Cann * stepOneEp (stepOneDelta (stepOneC1 d Cedos Cannp Citer k) alpha)) ≤ 1 / 2 * 3 ^ (-(1 / 4) * ↑k) → ∀ (L m n : ℤ), m ≤ L → m ≤ m0 → 14 ≤ m - n → ∀ v ∈ Support.latticeCubeSet d n m, Support.triadicLatticePoint n v ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d (m - 1)) → ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), GoodScaleWindows M stepOneSEighth (stepOneDelta (stepOneC1 d Cedos Cannp Citer k) alpha) stepOneSEighth_pos n m omega → ↑(stepThreeBadSet M (stepOneDelta (stepOneC1 d Cedos Cannp Citer k) alpha) n m (Support.triadicLatticePoint n v) omega).card ≤ stepOneDelta (stepOneC1 d Cedos Cannp Citer k) alpha * (↑m - ↑n + 1) → ∀ (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 (Support.triadicLatticePoint n v) m j) u.toFun (c j) (slope j)) → ∀ (n' m' : ℤ), n ≤ n' → ⋯

e.oscillation.iteration.result on the interior branch, hstep4 GONE.

For z = 3^n v ∈ □_{m-1} and every n ≤ n' ≤ m' ≤ m,

   3^{-n'} ‖u - (u)_{U_{n'}}‖_{L²(U_{n'})}
     ≤ C exp( C₁^{-1} C_iter (1-α)(m-n) ) ( 3^{-m'} ‖u - (u)_{U_{m'}}‖ + C·dataG )
       + C exp( C₁^{-1} C_iter (1-α)(m-n) ) · 0 ,
   dataG = 4 C_δ 3^{m/2} σ_m^{-1} ( K_g C_{S4.4}(d,1/4) ) / (1 - 3^{-(1/2-γ)}) ,

with U = stepThreeWindow z m, C_iter = 2C₀(k+1+C_ε), and NO Step-4 decay hypothesis: the excess decay is produced from the harmonic-approximation anchor and the Step-3 supply events.