HomSpineInstallData

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

The data slot and the gap absorption, at the finite-p window s₂ < 1/2

What this file supplies

Two of the three residues of HomSpineInstallArith's reduction are settled here, at the finite-p pin where s₂ is FORCED strictly below the printed 1/2 (the membership band 1/2 - d/p < s₂ < 1/2 of HomCGFinalDatum).

1. The data slot, PROVED. overlapSeminorm_toReal_le bounds the printed forcing carrier [𝐠] by C_data(d,s₂,p) · K_g · 3^{(1/2-s₂)m}, from the root's OWN C^{0,1/2} binder on 𝐠. This is the hDgbound residue; it is no longer a hypothesis of the assembly.
2. The gap absorption at general s₂. homGapAbsorbAt is the printed gap absorption with s₂ = 1/2 released:

     s^{-9/2} · 3^{s₂(n-m)} ≤ C_gap(s₂) · γ^5,
        C_gap(s₂) = 3125 (10 s₂ log 3 - 5)^{-5},
   

   valid exactly when 10 s₂ log 3 > 5, i.e. s₂ > (2 log 3)^{-1} = 0.4551….

THE LOAD-BEARING VERDICT (machine-checked below)

EthmB(m)'s second summand is C γ⁵(1 + 𝓔²), so the forcing leg must be absorbed at the γ⁵ rate. With the printed mesoscale k = ⌈10|log γ|⌉ the absorption's exponent condition is 10 s₂ log 3 > 5, and

• the numeral pin s₂ = 3/8 FAILS it (10·(3/8)·log 3 < 4.27 < 5). The pin cannot reach γ⁵;
• gapExponent_holds_at_fortyNineHundredths — s₂ = 49/100 SATISFIES it (10·(49/100)·log 3 > 5.15 > 5), and 49/100 is inside the membership band 1/4 < s₂ < 1/2 at the printed exponent p = 4d.

So the re-cut's numeral pin must move from s₂ = 3/8 to any s₂ ∈ ((2 log 3)^{-1}, 1/2); nothing else in the frame changes. This is a NUMERAL correction inside the own freedom (s₂ is existentially bound by the bundle), not a Theorem C dependence.

1. The data slot: the printed forcing carrier, from the root's binder

noncomputable def Algsuperdiff.Section4.Provider.Homogenization.cgOverlapDataConst (d : ℕ) (s2 : ↑HCPolySupport.FractionalOrder) (p : HCPolySupport.FiniteLpExponent) : ℝ

The data-slot constant C_data(d,s₂,p): the dimension-only overlap/fractional comparison constant times the Gagliardo radial constant of the C^{0,1/2} ⊂ W^{s₂,p} embedding. It depends on (d, s₂, p) only — never on the model, the scale or the data.

Equations

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

theorem Algsuperdiff.Section4.Provider.Homogenization.cgOverlapDataConst_nonneg (d : ℕ) (s2 : ↑HCPolySupport.FractionalOrder) (p : HCPolySupport.FiniteLpExponent) (hlo : 0 < (1 / 2 - ↑s2) * p.exponent.toReal) : 0 ≤ cgOverlapDataConst d s2 p

theorem Algsuperdiff.Section4.Provider.Homogenization.overlapSeminorm_toReal_le {d : ℕ} [NeZero d] (m : ℤ) (s2 : ↑HCPolySupport.FractionalOrder) (p : HCPolySupport.FiniteLpExponent) {Kg : ℝ} {g : HCPolySupport.Vec d → HCPolySupport.Vec d} (hKg0 : 0 ≤ Kg) (hlt : ↑s2 < 1 / 2) (hgt : 1 / 2 - ↑d / p.exponent.toReal < ↑s2) (hg : Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (1 / 2) Kg g) : (HCPolySupport.Book.Ch03.ABK26.cubeEuclideanPositiveBesovOverlapESeminorm (HCPolySupport.originCube d m) s2 p g).toReal ≤ cgOverlapDataConst d s2 p * Kg * 3 ^ ((1 / 2 - ↑s2) * ↑m)

THE DATA SLOT, PROVED.

The printed forcing carrier [𝐠]_{W^{s₂,p}(□_m)} — the overlap seminorm the coarse-graining display's second term carries — is at most C_data(d,s₂,p) · K_g · 3^{(1/2-s₂)m}, from the root's own C^{0,1/2} binder on 𝐠. The single scale power is the 1/2 - s₂ order loss of the embedding; against the display's 3^{s₂n} it reassembles into the printed 3^{s₂(n-m)}·3^{m/2} (HomSpineInstallArith.three_rpow_mesoscale_split).

2. The gap absorption at a general s₂

noncomputable def Algsuperdiff.Section4.Provider.Homogenization.homGapConstAt (s2 : ℝ) : ℝ

The gap-absorption constant at a general s₂, 3125(10 s₂ log 3 - 5)^{-5}, the printed s₂ = 1/2 constant with s₂ released.

Equations

• Algsuperdiff.Section4.Provider.Homogenization.homGapConstAt s2 = 3125 / (10 * s2 * Real.log 3 - 5) ^ 5

theorem Algsuperdiff.Section4.Provider.Homogenization.homGapAbsorbAt {d : ℕ} {M : Section3.ABKModel d} (hlog : 4 ≤ |Real.log M.gamma|) (hgamma1 : M.gamma < 1) (m : ℤ) {s2 : ℝ} (hs2 : 5 < 10 * s2 * Real.log 3) : homS M ^ (-(9 / 2)) * 3 ^ (s2 * (↑(homN M m) - ↑m)) ≤ homGapConstAt s2 * M.gamma ^ 5

The gap absorption, s₂ released.

  s^{-9/2} 3^{s₂(n-m)} ≤ C_gap(s₂) γ⁵,

with n = m - ⌈10|log γ|⌉ the printed mesoscale. The slack is 10 s₂ log 3 - 5, which is positive exactly when s₂ > (2 log 3)^{-1}; the printed s₂ = 1/2 has slack 5(log 3 - 1) > 0.

3. The numeral verdict on the s₂ pin

theorem Algsuperdiff.Section4.Provider.Homogenization.log_three_gt : 10529 / 10000 < Real.log 3

A machine-checked lower bound: log 3 > 1.0529.

theorem Algsuperdiff.Section4.Provider.Homogenization.gapExponent_holds_at_fortyNineHundredths : 5 < 10 * (49 / 100) * Real.log 3

THE VERDICT (b). The pin s₂ = 49/100 DOES satisfy it: 10·(49/100)·log 3 > 5. Together with 1/4 < 49/100 < 1/2 (the membership band at p = 4d) this is an admissible replacement.