HomSpineCloseRecut

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

Theorem B, §4.5: the Step-2b/3b re-cuts (hlevel, hS)

What this module is

The re-cut of the printed energy slot, needed because what Step 2b delivers is weighted rather than uniform in the depth index.

(a) The energy slot at the s₁ = s/4 pin — A MEASURED PRINT DEFECT

The printed ℓ^p energy slot is fed from a UNIFORM bound Gen R ≤ S. What Step 2b actually delivers is a WEIGHTED bound: at the §4.5 parameter web the family bound F j z ≤ K·3^{(1-α)(m-j)} (the Step-2b local family) grows like 3^{a i} in the depth index i = (m-n)+i with

  a = 1 - α = s/2.

The printed weight of the energy slot is 3^{-(s-s₁)p i}. So the summand is 3^{-((s-s₁)-a)p i} and the slot converges iff s₁ < s - a = s/2. The manuscript's s₁ = s/2 is EXACTLY the borderline: (s - s₁) - a = 0, every summand is the same, the partial sums grow linearly in N, and NO S-bound survives. The s₁ = s/2 gap is 0, while the s₁ = s/4 gap is s/4 > 0.

The choice below is free at the hypothesis level and stays inside the printed range s₁ ∈ (0,s) of the source proposition itself — it is a choice the printed statement already offers, i.e. pre-authorized s-power territory, not a statement change:

  s₁:= s/4    ⟹    (s - s₁) - a = 3s/4 - s/2 = s/4 > 0.

coarseGrainingEnergyPartial_le_of_weightedBound is the weighted-hypothesis variant; coarseGrainingEnergyPartial_le_at_quarterPin is its instance at the pin. The price is the explicit geometric factor (1 - 3^{-((w-a)p)})^{-1/p} in place of (1 - 3^{-(wp)})^{-1/p}, i.e. a displayed constant and nothing else.

(b) THE ν VERSUS σ SEAM — NOTED, NOT CONVERTED

The printed energy slot sums ‖σ^{1/2}∇u‖_{L²(z+□_k)}^p (transcribed in HomFinitePSource), while Step 2b's family is the manuscript's ν^{1/2}‖∇u‖_{L²(z+□_j)}. The printed σ of the energy slot is UNSUBSCRIPTED and therefore ambiguous between

• the coefficient field's own symmetric part — here symmPart a_L = ν Id, in which case ‖σ^{1/2}∇u‖ = ν^{1/2}‖∇u‖ and the Step-2b family feeds the slot with NO conversion; and
• the constant comparator σ₀ = σ_m, in which case feeding the Step-2b family into the slot would require a ν ↔ σ conversion.

This module refuses the second reading and performs NO conversion: the per-cube energy Gen is left ABSTRACT in every statement below (as it is in the transcribed printed proposition), so the caller pins it, and the units doctrine is not touched anywhere in this file. The seam is reported, not crossed.

3. The energy slot from a WEIGHTED Step-2b family bound

theorem Algsuperdiff.Section4.Provider.Homogenization.coarseGrainingEnergyPartial_le_of_weightedBound {d : ℕ} {Q : HCPolySupport.TriadicCube d} {p w a S : ℝ} {jn N : ℕ} {Gen : HCPolySupport.TriadicCube d → ℝ} (hp : 0 < p) (haw : a < w) (hS : 0 ≤ S) (hG : ∀ (i : ℕ), ∀ R ∈ HCPolySupport.descendantsAtDepth Q (jn + i), Gen R ≤ S * 3 ^ (a * ↑i)) (hG0 : ∀ (R : HCPolySupport.TriadicCube d), 0 ≤ Gen R) : coarseGrainingEnergyPartial Q p w jn N Gen ≤ S * coarseGrainingGeomFactor p (w - a)

The finite-p energy slot from the WEIGHTED Step-2b datum.

The unweighted form of the slot bound asks for a UNIFORM per-cube bound Gen R ≤ S. What Step 2b delivers is Gen R ≤ S·3^{a i} at depth jn + i. As long as the printed weight strictly dominates that growth (a < w, i.e. s₁ < s - (1-α)), the slot is still bounded by S times an explicit geometric factor, now at the GAP exponent w - a.

Gen is abstract here: no coefficient field, no ν, no σ (see the module docstring's seam disclosure).

theorem Algsuperdiff.Section4.Provider.Homogenization.coarseGrainingEnergyPartial_le_at_quarterPin {d : ℕ} {Q : HCPolySupport.TriadicCube d} {p s S : ℝ} {jn N : ℕ} {Gen : HCPolySupport.TriadicCube d → ℝ} (hp : 0 < p) (hs : 0 < s) (hS : 0 ≤ S) (hG : ∀ (i : ℕ), ∀ R ∈ HCPolySupport.descendantsAtDepth Q (jn + i), Gen R ≤ S * 3 ^ (s / 2 * ↑i)) (hG0 : ∀ (R : HCPolySupport.TriadicCube d), 0 ≤ Gen R) : coarseGrainingEnergyPartial Q p (s - s / 4) jn N Gen ≤ S * coarseGrainingGeomFactor p (s / 4)

The energy slot at the s₁ = s/4 pin.

The Step-2b family grows like 3^{(s/2) i} (the §4.5 web's 1 - α = s/2), the printed weight at s₁ = s/4 is 3^{-(3s/4)p i}, and the gap is s/4 > 0. This is the instance of coarseGrainingEnergyPartial_le_of_weightedBound the Step-3/Step-4 chain consumes; the printed s₁ = s/2 would give gap 0 and no bound.