HomSeamSpineBudget

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

The root display chain: the |log γ|³ collapse and its free factor slot

What this file supplies

The corrected statement enlarges the moment display of Theorem B from |log γ|² to |log γ|³ and assigns the new log to the two machine-pinned costs of realizing Step 3 at the fixed exponent p = 4d. This file is the display-side half of that assignment.

The seam display (HomSeamStepOneDisplay.exists_ethmB_seam_moment_bound) gives the FIRST TWO logs and is untouched: StepOneDisplayAt is consumed here verbatim, at Real.log M.gamma ^ (2: ℕ). What changes is the K_abs slot of the real cut: it is no longer a model-free numeral but a per-model quantity carrying an explicit BUDGET

  0 ≤ K_abs   and   K_abs ≤ C_abs · |log γ|,

and the produced E_B moment display therefore gives at

  C · (√p + √|log γ|) · √γ · |log γ|³,

which is the frozen statement's shape. The budget is exactly what HomSeamBudgetArith.recut_geomBudget_le_absLog certifies for GEOM · CA.

  exists_spine_defect_witness_of_displayBudget    -- the real cut, at |log γ|³
  homogenization_spine_close_of_stepOneDisplayBudget
                                                  -- the spine, (C1) discharged

Passing from |log γ|² to |log γ|³ at the level of these statements is a one-log weakening (the printed gate gives 4 ≤ |log γ|, so |log γ|² ≤ |log γ|³); nothing here is stronger than the chain, and the extra log is spent, not banked.

1. The real defect witness, at the budgeted K_abs

theorem Algsuperdiff.Section4.Provider.Homogenization.exists_spine_defect_witness_of_displayBudget (d : ℕ) (cstar : ℝ) (_hcstar : 0 < cstar) {Cgap Cabs C0 : ℝ} (hCgap : 0 ≤ Cgap) (hCabs : 0 ≤ Cabs) (hC0 : 1 ≤ C0) : ∃ (gamma0 : ℝ) (C : ℝ), 0 < gamma0 ∧ 0 < C ∧ ∀ (M : Section3.ABKModel d), Section3.Disorder.cstar M = cstar → M.gamma ≤ gamma0 → ∀ (Kabs : ℝ), 0 ≤ Kabs → Kabs ≤ Cabs * |Real.log M.gamma| → ∀ (Y : Section3.Cutoff.CutoffSample d → ENNReal), Measurable Y → ∀ (m : ℤ) (sb : { s : ℝ // 0 < s }), StepOneDisplayAt M Cgap Y m sb C0 → ∃ (EB : Section3.Cutoff.CutoffSample d → ℝ), (∀ (omega : Section3.Cutoff.CutoffSample d), 0 ≤ EB omega) ∧ Measurable EB ∧ (∀ (p : ℝ), 1 ≤ p → p ≤ C⁻¹ * M.gamma⁻¹ * |Real.log M.gamma|⁻¹ → ∫⁻ (omega : Section3.Cutoff.CutoffSample d), ENNReal.ofReal (EB omega) ^ p ∂↑(Section3.Cutoff.cutoffSampleLaw M) ≤ ENNReal.ofReal (C * (√p + √|Real.log M.gamma|) * √M.gamma * |Real.log M.gamma| ^ 3) ^ p) ∧ ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), ∀ (D : ℝ), 0 ≤ D → ENNReal.ofReal D ≤ ethmB M Cgap Y m (homN M m) sb omega → Kabs * D ≤ EB omega

The real defect witness at the frozen display.

The real defect witness at a free display, with the K_abs slot moved INSIDE the model quantifier and gated by the budget K_abs ≤ C_abs · |log γ|. The Step-1 display hypothesis is unchanged, at |log γ|²; the conclusion is the frozen moment display, at |log γ|³.

The one new inequality is K_abs · (C₀(1+C_gap) T |log γ|²) ≤ C · T · |log γ|³ — the free factor slot, spent on the budget and on nothing else.

2. The spine at the frozen display, with (C1) discharged

theorem Algsuperdiff.Section4.Provider.Homogenization.homogenization_spine_close_of_stepOneDisplayBudget (d : ℕ) [NeZero d] (cstar : ℝ) (hcstar : 0 < cstar) {Cgap Cabs C0 : ℝ} (hCgap : 0 ≤ Cgap) (hCabs : 0 ≤ Cabs) (hC0 : 1 ≤ C0) : ∃ (gamma0 : ℝ) (C : ℝ), 0 < gamma0 ∧ 0 < C ∧ ∀ (M : Section3.ABKModel d), Section3.Disorder.cstar M = cstar → M.gamma ≤ gamma0 → ∀ (Kabs : ℝ), 0 ≤ Kabs → Kabs ≤ Cabs * |Real.log M.gamma| → ∀ (Y : Section3.Cutoff.CutoffSample d → ENNReal), Measurable Y → ∀ (m : ℤ) (sb : { s : ℝ // 0 < s }), StepOneDisplayAt M Cgap Y m sb C0 → (∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), HomSpineClauseSupplierAtGrad M Cgap Y m sb (↑(Section3.Annealed.sigmaBar M m)) Kabs omega) → ∃ (sigmaBar : ℝ), 0 < sigmaBar ∧ |sigmaBar - √(M.nu ^ 2 + cstar * M.gamma⁻¹ * Real.rpow 3 (2 * M.gamma * ↑m))| ≤ C * √M.gamma * |Real.log M.gamma| * sigmaBar ∧ ∃ (EB : Section3.Cutoff.CutoffSample d → ℝ), (∀ (omega : Section3.Cutoff.CutoffSample d), 0 ≤ EB omega) ∧ Measurable EB ∧ (∀ (p : ℝ), 1 ≤ p → p ≤ C⁻¹ * M.gamma⁻¹ * |Real.log M.gamma|⁻¹ → ∫⁻ (omega : Section3.Cutoff.CutoffSample d), ENNReal.ofReal (EB omega) ^ p ∂↑(Section3.Cutoff.cutoffSampleLaw M) ≤ ENNReal.ofReal (C * (√p + √|Real.log M.gamma|) * √M.gamma * |Real.log M.gamma| ^ 3) ^ p) ∧ ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), ∀ (L : ℤ), m ≤ L → ∀ (u v h : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) (g : HCPolySupport.Vec d → HCPolySupport.Vec d) (Kg Kh KhInf : ℝ), Support.IsDirichletSolutionOn (Section3.Cutoff.coefficientCutoff M.nu L omega).toCoeffField (HCPolySupport.originCube d m) u h g → Support.IsDirichletSolutionOn (fun (x : HCPolySupport.Vec d) => sigmaBar • 1) (HCPolySupport.originCube d m) v h g → Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (1 / 2) Kg g → Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (1 / 2) Kh h.grad → (∀ x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m), ‖h.grad x‖ ≤ KhInf) → Support.HasGradientOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) h.toFun h.grad → (∀ᵐ (x : HCPolySupport.Vec d) ∂MeasureTheory.volume.restrict (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)), Real.rpow 3 (-↑m) * |u.toFun x - v.toFun x| ≤ EB omega * (sigmaBar⁻¹ * Real.rpow 3 (↑m / 2) * Kg + (KhInf + Real.rpow 3 (↑m / 2) * Kh))) ∧ |(HCPolySupport.volumeAverage (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) fun (y : HCPolySupport.Vec d) => M.nu * HCPolySupport.vecNormSq (u.grad y)) - HCPolySupport.volumeAverage (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) fun (y : HCPolySupport.Vec d) => sigmaBar * HCPolySupport.vecNormSq (v.grad y)| ≤ EB omega * (√sigmaBar⁻¹ * Real.rpow 3 (↑m / 2) * Kg + √sigmaBar * (KhInf + Real.rpow 3 (↑m / 2) * Kh)) ^ 2

The spine at a free (Y, sb) and the budgeted K_abs, at |log γ|³.

HomSeamGradSpine's gradient-threaded spine close with

• the K_abs slot moved inside the model quantifier and gated by the budget,
• the produced moment clause at the frozen factor |log γ|³,

and with clause (C1) discharged off the Section-3 anchor Algsuperdiff.Frozen.Section3.induction_bounds at the genuine running diffusivity Annealed.sigmaBar M m, exactly as in the original. The Step-1 display hypothesis, the clause supplier and the root's own HasGradientOn binder are unchanged, byte for byte.