StepSixBoundaryIterationC1

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

1. The three constants of the boundary Step-4 output

noncomputable def Algsuperdiff.Section4.Provider.Regularity.edBoundaryCbd (d : ℕ) [NeZero d] (Cb C : ℝ) (k : ℕ) : ℝ

The boundary δ's g-leg constant C_bd produced's slot.

Equations

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

noncomputable def Algsuperdiff.Section4.Provider.Regularity.edBoundaryCah (d : ℕ) [NeZero d] (Cb C : ℝ) (k : ℕ) : ℝ

The boundary δ's ∇h-leg constant C_ah.

Equations

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

noncomputable def Algsuperdiff.Section4.Provider.Regularity.edBoundaryCeps (d : ℕ) [NeZero d] (Cb C : ℝ) (k : ℕ) : ℝ

The boundary ε-leg coefficient C_ε.

Equations

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

theorem Algsuperdiff.Section4.Provider.Regularity.edBoundaryCbd_nonneg (d : ℕ) [NeZero d] (Cb : ℝ) {C : ℝ} (hC : 0 ≤ C) (k : ℕ) : 0 ≤ edBoundaryCbd d Cb C k

theorem Algsuperdiff.Section4.Provider.Regularity.edBoundaryCah_nonneg (d : ℕ) [NeZero d] (Cb : ℝ) {C : ℝ} (hC : 0 ≤ C) (k : ℕ) : 0 ≤ edBoundaryCah d Cb C k

theorem Algsuperdiff.Section4.Provider.Regularity.edBoundaryCeps_nonneg (d : ℕ) [NeZero d] (Cb : ℝ) {C : ℝ} (hC : 0 ≤ C) (k : ℕ) : 0 ≤ edBoundaryCeps d Cb C k

2. The boundary dataH, and its two Step-6 legs

noncomputable def Algsuperdiff.Section4.Provider.Regularity.edBoundaryDataH (d : ℕ) [NeZero d] (Cb C : ℝ) (k : ℕ) (Kh Se : ℝ) (m : ℤ) : ℝ

The boundary ∇h leg of e.sum.delta.j.bound —'s α-free grouping, with NO ε-free flat summand:

   dataH_∂ = C_ah·3^{m/2}(1+C_gag)K_h/(1-3^{-1/2})  +  S_ε·(2 C_bd 3^{m/2} K_h) .

Equations

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

theorem Algsuperdiff.Section4.Provider.Regularity.edBoundaryKhleg_nonneg (d : ℕ) [NeZero d] (Cb : ℝ) {C Kh : ℝ} (hC : 0 ≤ C) (k : ℕ) (hKh : 0 ≤ Kh) (m : ℤ) : 0 ≤ edBoundaryCah d Cb C k * (3 ^ (↑m / 2) * (Kh * (1 + stepFourGagliardoConst d stepOneS))) / (1 - stepFiveRatioH)

theorem Algsuperdiff.Section4.Provider.Regularity.edBoundaryHinf_nonneg (d : ℕ) [NeZero d] (Cb : ℝ) {C Kh : ℝ} (hC : 0 ≤ C) (k : ℕ) (hKh : 0 ≤ Kh) (m : ℤ) : 0 ≤ 2 * edBoundaryCbd d Cb C k * (Real.rpow 3 (↑m / 2) * Kh)

theorem Algsuperdiff.Section4.Provider.Regularity.edBoundaryDataH_nonneg (d : ℕ) [NeZero d] (Cb : ℝ) {C Kh Se : ℝ} (hC : 0 ≤ C) (k : ℕ) (hKh : 0 ≤ Kh) (hSe : 0 ≤ Se) (m : ℤ) : 0 ≤ edBoundaryDataH d Cb C k Kh Se m

3. e.oscillation.iteration.result on the boundary branch

theorem Algsuperdiff.Section4.Provider.Regularity.edFinal_oscillationIterationResult_boundaryC1 (d : ℕ) [NeZero d] (hd : d ≠ 0) : ∃ (C : ℝ) (Ccap : ℝ) (Cb : ℝ) (Cann : ℝ), 0 < C ∧ 0 < Ccap ∧ 0 ≤ Cb ∧ 0 < Cann ∧ ∃ (k₀ : ℕ), 3 ≤ k₀ ∧ ∀ (k : ℕ), k₀ ≤ 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 ≤ Ccap⁻¹ * Section3.Disorder.cstar M ^ 10 → M.gamma ≤ Cann⁻¹ * Section3.Disorder.cstar M ^ 10 → M.gamma ≤ 1 / 256 → ∀ (Cedos Cannp alpha : ℝ), alpha ≤ 1 → stepOneDelta (stepOneC1 d Cedos Cannp Citer (k + 1)) alpha ∈ Set.Ioc 0 (1 / 2) → stepOneDelta (stepOneC1 d Cedos Cannp Citer (k + 1)) alpha ≤ 64 * (C ^ 2)⁻¹ * stepOneS ^ 6 → M.gamma * |Real.log M.gamma| ^ 2 ≤ stepOneSEighth.rpow (3 / 2) * Section3.Disorder.cstar M ^ 2 * stepOneEp (stepOneDelta (stepOneC1 d Cedos Cannp Citer (k + 1)) alpha) → ExcessDecay.edBridgeEpsConstGen d (max (ExcessDecay.Schauder.schauderWindowConst d) Cb) C k * Ccap * stepOneS.rpow (-3) * √(stepOneDelta (stepOneC1 d Cedos Cannp Citer (k + 1)) alpha) ≤ 1 / 2 * 3 ^ (-(1 / 4) * (↑k + 1)) → ∀ (L m n : ℤ), m ≤ L → m ≤ m0 → 14 ≤ m - n → ∀ v ∈ Support.latticeCubeSet d n m, ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), GoodScaleWindows M stepOneSEighth (stepOneDelta (stepOneC1 d Cedos Cannp Citer (k + 1)) alpha) stepOneSEighth_pos n m omega → ↑(stepThreeBadSet M (stepOneDelta (stepOneC1 d Cedos Cannp Citer (k + 1)) alpha) n m (Support.triadicLatticePoint n v) omega).card ≤ stepOneDelta (stepOneC1 d Cedos Cannp Citer (k + 1)) alpha * (↑m - ↑n + 1) → ∀ (u hdat : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) (g : HCPolySupport.Vec d → HCPolySupport.Vec d) (Kg Kh : ℝ), 0 ≤ Kg → 0 ≤ Kh → 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 → Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (1 / 2) Kh hdat.grad → ⋯

e.oscillation.iteration.result printed lattice centre, hstep4 GONE.

The interior endpoint's sibling off's boundary Step-4 slot: no interiority gate, the contraction over k+1 scales, and the nonzero boundary dataH_∂.

4. The boundary Step 6, in the chain's hosc shape

noncomputable def Algsuperdiff.Section4.Provider.Regularity.edBoundaryDataHPrinted (d : ℕ) [NeZero d] (Cb C : ℝ) (k : ℕ) (Kh : ℝ) (m : ℤ) : ℝ

The printed boundary ∇h datum leg — α-free, γ-free, δ-free, and a multiple of 3^{m/2} K_h:

   dataH^print_∂ = C_ah·3^{m/2}(1+C_gag)K_h/(1-3^{-1/2})
                     + (4/log 3)·(2 C_bd 3^{m/2} K_h) .

The absolute constant 4/log 3 is the price's ε-funded absorption; no (1-α)^{-1} occurs, because's boundary δ carries no ε-free flat summand.

Equations

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

theorem Algsuperdiff.Section4.Provider.Regularity.stepSixBoundary_oscSlot_of_epsFunded (d : ℕ) {Cedos Cann Citer C alpha : ℝ} {k : ℕ} {n m : ℤ} {oscLo oscHi dataG Khleg Hinf Se : ℝ} (hC : 0 ≤ C) (hCiter : 0 ≤ Citer) (halpha : alpha ≤ 1) (hnm : n ≤ m) (hoscHi : 0 ≤ oscHi) (hdataG : 0 ≤ dataG) (hKhleg : 0 ≤ Khleg) (hHinf : 0 ≤ Hinf) (hSe0 : 0 ≤ Se) (hSe : Se ≤ 2 * stepOneDelta (stepOneC1 d Cedos Cann Citer k) alpha * (↑m - ↑n)) (hiter : oscLo ≤ C * Real.exp ((stepOneC1 d Cedos Cann Citer k)⁻¹ * Citer * stepSixExponent alpha n m) * (oscHi + C * dataG) + C * Real.exp ((stepOneC1 d Cedos Cann Citer k)⁻¹ * Citer * stepSixExponent alpha n m) * (Khleg + Se * Hinf)) : oscLo ≤ (C + C * C) * Real.rpow 3 (1 / 2 * stepSixExponent alpha n m) * oscHi + (C + C * C) * Real.rpow 3 (1 / 2 * stepSixExponent alpha n m) * (dataG + (Khleg + 4 / Real.log 3 * Hinf))

t.regularity Step 6 on the boundary branch, in the Step-7 chain's own hosc slot.

The ε-funded absorption at ind := 1, re-grouped so the produced data leg is a single dataG + dataH^print_∂ bracket at one constant C + C² — exactly the shape StepSevenCaccFinalChain's hosc reads (there at H = 0).

theorem Algsuperdiff.Section4.Provider.Regularity.edFinal_oscillationHolderBound_boundaryC1 (d : ℕ) [NeZero d] (hd : d ≠ 0) : ∃ (C : ℝ) (Ccap : ℝ) (Cb : ℝ) (Cann : ℝ), 0 < C ∧ 0 < Ccap ∧ 0 ≤ Cb ∧ 0 < Cann ∧ ∃ (k₀ : ℕ), 3 ≤ k₀ ∧ ∀ (k : ℕ), k₀ ≤ 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 ≤ Ccap⁻¹ * Section3.Disorder.cstar M ^ 10 → M.gamma ≤ Cann⁻¹ * Section3.Disorder.cstar M ^ 10 → M.gamma ≤ 1 / 256 → ∀ (Cedos Cannp alpha : ℝ), alpha ≤ 1 → stepOneDelta (stepOneC1 d Cedos Cannp Citer (k + 1)) alpha ∈ Set.Ioc 0 (1 / 2) → stepOneDelta (stepOneC1 d Cedos Cannp Citer (k + 1)) alpha ≤ 64 * (C ^ 2)⁻¹ * stepOneS ^ 6 → M.gamma * |Real.log M.gamma| ^ 2 ≤ stepOneSEighth.rpow (3 / 2) * Section3.Disorder.cstar M ^ 2 * stepOneEp (stepOneDelta (stepOneC1 d Cedos Cannp Citer (k + 1)) alpha) → ExcessDecay.edBridgeEpsConstGen d (max (ExcessDecay.Schauder.schauderWindowConst d) Cb) C k * Ccap * stepOneS.rpow (-3) * √(stepOneDelta (stepOneC1 d Cedos Cannp Citer (k + 1)) alpha) ≤ 1 / 2 * 3 ^ (-(1 / 4) * (↑k + 1)) → ∀ (L m n : ℤ), m ≤ L → m ≤ m0 → 14 ≤ m - n → ∀ v ∈ Support.latticeCubeSet d n m, ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), GoodScaleWindows M stepOneSEighth (stepOneDelta (stepOneC1 d Cedos Cannp Citer (k + 1)) alpha) stepOneSEighth_pos n m omega → ↑(stepThreeBadSet M (stepOneDelta (stepOneC1 d Cedos Cannp Citer (k + 1)) alpha) n m (Support.triadicLatticePoint n v) omega).card ≤ stepOneDelta (stepOneC1 d Cedos Cannp Citer (k + 1)) alpha * (↑m - ↑n + 1) → ∀ (u hdat : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) (g : HCPolySupport.Vec d → HCPolySupport.Vec d) (Kg Kh : ℝ), 0 ≤ Kg → 0 ≤ Kh → 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 → Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (1 / 2) Kh hdat.grad → ⋯

e.oscillation.Holder.bound printed lattice centre.

edFinal_oscillationIterationResult_boundaryC1 composed with the boundary Step 6: the interior endpoint's shape with the same dataG and a nonzero printed dataH^print_∂.

5. The two boundary funding floors

theorem Algsuperdiff.Section4.Provider.Regularity.edBoundary_deltaCap_of_c1_floor {C C1 alpha : ℝ} (hC : 0 < C) (halpha0 : 0 ≤ alpha) (hC1 : 0 < C1) (hfloor : 64 * C ^ 2 ≤ C1) : stepOneDelta C1 alpha ≤ 64 * (C ^ 2)⁻¹ * stepOneS ^ 6

The boundary Step-4 δ-cap, from a pure C₁-floor.

stepFourDecay_boundary_pinned's δ-cap δ ≤ 64C^{-2}s^6 is met by every δ = C₁^{-1}(1-α) with α ≥ 0 once C₁ ≥ 64C², because s = 1/4 makes the cap exactly (64C²)^{-1}.

theorem Algsuperdiff.Section4.Provider.Regularity.edBridgeEpsConstGen_nonneg' (d : ℕ) {Cs C : ℝ} (hCs : 0 ≤ Cs) (hC : 0 ≤ C) (k : ℕ) : 0 ≤ ExcessDecay.edBridgeEpsConstGen d Cs C k

noncomputable def Algsuperdiff.Section4.Provider.Regularity.edBoundaryFundFloor (d : ℕ) [NeZero d] (Cb C Ccap : ℝ) (k : ℕ) : ℝ

The boundary Step-4 smallness gate, from a pure C₁-floor.

RootClauseBFinalFunding.edFunding_of_c1_floor's sibling for the boundary lane: the gate

   C_{eps,gen}(d,C_s,C,k)·C_cap·s^{-3}·√δ  ≤  ½·3^{-(k+1)/4}

holds at every δ = C₁^{-1}(1-α) with α ≥ 0 once C₁ clears the explicit floor (2·C_{eps,gen}·C_cap·s^{-3}·3^{(k+1)/4})². No division and no positivity of the constant is needed — the argument is √δ ≤ (√C₁)^{-1} and one cross multiplication.

Equations

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

theorem Algsuperdiff.Section4.Provider.Regularity.edBoundaryFunding_of_c1_floor (d : ℕ) [NeZero d] {Cb C Ccap C1 alpha : ℝ} {k : ℕ} (hC : 0 ≤ C) (hCcap : 0 ≤ Ccap) (halpha0 : 0 ≤ alpha) (hC1 : 0 < C1) (hfloor : edBoundaryFundFloor d Cb C Ccap k ≤ C1) : ExcessDecay.edBridgeEpsConstGen d (max (ExcessDecay.Schauder.schauderWindowConst d) Cb) C k * Ccap * stepOneS.rpow (-3) * √(stepOneDelta C1 alpha) ≤ 1 / 2 * 3 ^ (-(1 / 4) * (↑k + 1))