HomSpineFinalEndpoint #

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

Theorem B, §4.5: THE SPINE — the frozen root's conclusion body #

  ∃ γ₀ C, 0 < γ₀ ∧ 0 < C ∧ ∀ M, c⋆(M) = c⋆ → γ ≤ γ₀ → ∀ m,
    ∃ σ_m, 0 < σ_m ∧ (C1) ∧
      ∃ E_B, (0 ≤ E_B) ∧ Measurable E_B ∧ (C2) ∧
        ∀ᵐ ω, ∀ L ≥ m, ∀ u v h g K_g K_h K_h^∞, (five binders) → (C3) ∧ (C4).

What is DISCHARGED here, and what is supplied #

(C1) — the σ_m closeness display: supplied at the constant C_flow and re-based to the endpoint's own C = C_wit + C_flow. This is Section 3's diffusivity_asymptotics (Frozen/Section3/DiffusivityAsymptotics.lean) read at σ_m = Annealed.sigmaBar M m; the endpoint is stated for an ARBITRARY σ_m satisfying it, so the Section-3 anchor plugs in unchanged, and so does the trivial witness σ_m = √(ν² + c⋆γ⁻¹3^{2γm}) (for which the display holds at every C ≥ 0). Nothing about σ_m is assumed beyond positivity and that one display.
(C2) — the real cut E_B = K·(EthmB(m)).toReal, its measurability, its moment at the root's own constant shape and p-range. Its own single edge is hY.
(C3), (C4) — supplied per ω by the clause supplier, at the EthmB(m)-domination interface: the producer exhibits a REAL defect D with ofReal D ≤ EthmB(m)(ω) (this is the manuscript's "comparing to the definition of EthmB(m)") and the two printed displays at K·D. The endpoint converts K·D into E_B(ω) through the witness's linkage — which is where the a.e. finiteness of the [0,∞] carrier is spent — and produces the root's clause bodies verbatim.

The data-bracket nonnegativity, derived (not assumed) #

The stepFourEnergyEndpoint carries 0 ≤ dataBracket … as a binder. Here it is PROVED from the root's own five binders: □_m contains two distinct points (exists_ne_pair_openCubeSet), so HolderSeminormBoundOn.nonneg gives 0 ≤ K_g and 0 ≤ K_h, and the sup binder at the cube centre gives 0 ≤ K_h^∞. No frame item is left on the data side.

The conditional set of the spine endpoint, itemized #

hY — the Theorem-C minimal-scale exponential moment (hC), exactly the edge, at the abstract [0,∞] carrier. See HomSpineFinalWitness for the blocked composition with the homY_moment_bound_of_gamma_le (a NAME COLLISION in the tree, reported there).
hC1 — the σ_m closeness display (Section 3's own anchor, or the trivial witness).
hclauses — the per-ω clause supplier. HomSpineFinalStepFour's exists_comparator_stepFourEnergy produces its (C4) half from ONE hCG' application and the Schauder external; its (C3) half is the L^∞ conversion at the same hCG'. What is NOT bridged here is the comparator quantifier (∃ v produced by the Schauder package versus the root's ∀ v) and the hlevel/hS arithmetic that consumes hC's display; both are itemized in this file.

1. Two distinct points of an open cube #

source

theorem Algsuperdiff.Section4.Provider.Homogenization.exists_ne_pair_openCubeSet {d : ℕ} [NeZero d] (Q : HCPolySupport.TriadicCube d) :

∃ (x : HCPolySupport.Vec d) (y : HCPolySupport.Vec d), x ∈ HCPolySupport.openCubeSet Q ∧ y ∈ HCPolySupport.openCubeSet Q ∧ x ≠ y

An open triadic cube in dimension d ≥ 1 contains two distinct points: its centre and the centre shifted by half a radius in every coordinate. This is all that is needed to turn the root's Hölder binders into 0 ≤ K_g, 0 ≤ K_h.

source

theorem Algsuperdiff.Section4.Provider.Homogenization.dataBracket_nonneg_of_binders {d : ℕ} [NeZero d] {m : ℤ} {sigmaBarM Kg Kh KhInf : ℝ} {h : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))} {g : HCPolySupport.Vec d → HCPolySupport.Vec d} (hsig : 0 < sigmaBarM) (hKg : Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (1 / 2) Kg g) (hKh : Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (1 / 2) Kh h.grad) (hKhInf : ∀ x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m), ‖h.grad x‖ ≤ KhInf) :

0 ≤ dataBracket sigmaBarM (Real.rpow 3 (↑m / 2)) Kg KhInf Kh

The printed data bracket is nonnegative under the root's own five binders.