AggregationRemainder

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

Provider: the remainder arithmetic of the localization good-event aggregation

After the σ-switch and the δ = 1 sensitivity injection, the good-event leg of e.mathcal.E.breakdown carries a per-cube additive remainder. Summing it over z ∈ 3^l ℤ^d ∩ □_m and over the localization weights c_{2s} 3^{-s(m-l)} produces the fifth summand of e.localization.mathcalE.estimate --- the printed

C γ² (h² + s^{-2} + E⁴ |log γ|⁴).

This module carries exactly that scalar collapse, and nothing else. It is purely deterministic real analysis: no measures, no Γ-Orlicz layer, no coefficient fields, no cubes. Everything below is a statement about the real series Σ_{j ∈ ℕ} 3^{-s j} (…) at j = m - l.

This is a provider endpoint only. It is not a source node, not a frozen declaration, and it closes no fraction of l.localization.mathcalE.

The corrected per-cube remainder, and two divergences from the print

• The printed per-cube display ends with C min{γ²Δ², 3^{2γΔ}} +⁴γ²|log γ|⁴ at Δ = m - l + h. Since u² ≤ 3^{2u} for u ≥ 0, that minimum is identically γ²Δ², which is strictly stronger than what the quoted input (e.switchtheshoms.betterer.again, whose right side carries an uncancelled 3^{γΔ}, squared by the e.shaking.lambda remainder) yields, and it is false for large Δ. The corrected per-cube remainder --- the one this module sums --- is C min{γ²Δ², 1} · 3^{2γΔ} +⁴γ²|log γ|⁴ · 3^{2γΔ}. It is carried here by switchRemainder. Note the manuscript itself uses the corrected min one display later.

• The fifth summand's constant is C(d, c⋆), not a pure C(d). That divergence does not arise here. The c⋆-dependence enters through the per-cube constant of the switch step (the hpre-style ellipticity witness), i.e. through the caller's C in localization_remainder_series_le_of_termwise; the collapse proved in this module multiplies that C through unchanged and contributes an absolute numerical factor 1024, with no dependence on d, on c⋆, or on any coarse-grained ellipticity witness. Callers must still record the c⋆-dependence they bring in.

Honest arithmetic versus the printed proof

The printed target is C γ²(h² + s^{-2} + E⁴|log γ|⁴) and the printed device is

Since s ≥ 8γ and 3^{-sγ^{-1}} ≤ C s^{-2} γ², we have c_{2s} Σ_l 3^{-s(m-l)} min{γ²(m-l+h)², 1} 3^{2γ(m-l+h)} ≤ C(h² + s^{-2})γ².

Achieved here: the printed shape, at the absolute constant 1024, with the E-leg included. Precisely, localization_remainder_series_le gives

c_{2s} Σ_{j ≥ 0} 3^{-sj}(min{γ²(j+h)²,1} + E⁴γ²|log γ|⁴) 3^{2γ(j+h)} ≤ 1024 γ² (h² + s^{-2} + E⁴|log γ|⁴),

for every s ∈ [8γ, 1], γ > 0, h ∈ ℕ with γ h ≤ 1. Two deviations from the printed derivation are recorded, both in the direction of less loss:

1. Summed honestly it contributes c_{2s} · E⁴γ²|log γ|⁴ · 3^{2γh} (1 - 3^{-(s-2γ)})^{-1} ≤ 27 E⁴γ²|log γ|⁴, the 27 = 3 × 9 coming from c_{2s} ≤ 3 c_{s-2γ} and 3^{2γh} ≤ 9 (γ h ≤ 1). The amplitude carries the load-bearing γ² and no s power.

2. The printed split is not needed. The printed proof splits the min at the index where γ(j+h) ≥ 1 and absorbs the tail with 3^{-sγ^{-1}} ≤ C s^{-2} γ². Reindexing exactly --- absorbing 3^{2γj} into 3^{-sj} to the lossless ratio q = 3^{-(s-2γ)}, which is < 1 because s ≥ 8γ --- makes the quadratic series converge outright: min{γ²(j+h)²,1} ≤ γ²(j+h)² ≤ 2γ²((j+1)² + h²) and Σ_j (j+1)² q^j ≤ 2(1-q)^{-3}. No case split, no cutoff index, no absorption inequality. The printed device is therefore sufficient but not necessary, and is not consumed by the collapse. This is a presentational observation about the printed proof, not a defect in it. The lossy alternative is real: replacing the min by the linear envelope min{a²,1} ≤ a (valid for a ≥ 0) collapses to C(γ h + γ s^{-1}). That claim is false and is withdrawn. The frozen unit-M Γ₂ amplitude is Cms · E · s^{-1} · √(ε γ) (Algsuperdiff/Frozen/Section3/MultiscaleEstimate.lean), which squares to Cms² · ε · E² · γ · s^{-2}; dividing the linear-envelope bound by it leaves Cs · Cev · (h s² + s) ≤ Cms² ε E², and the frozen parameter window (Disorder.cstar M)^{-1} · ε^{-Cms} ≤ E gives ε E² ≥ ε^{1-2Cms} c⋆^{-2}, unboundedly large as ε ↓ 0 for Cms > 1/2, against h ≍ Cms |log ε|. So the γ¹ shape clears the budget as well: the γ-power heuristic silently dropped the ε/E factors that actually supply the margin. The genuine reason the quadratic route is required is fidelity: the printed fifth summand is C γ²(h² + s^{-2} + E⁴|log γ|⁴), so a γ¹ result would be a different, weaker statement than the one this module must deliver. "The quadratic route is what buys the γ²" is the correct sentence; the budget justification for it is not.

Where the constants come from

c_{2s} = 1 - 3^{-2s} ≤ 3 (1 - 3^{-(s-2γ)}) = 3 c_{s-2γ} (needs s ≥ 6γ; the factorization 1 - q³ = (1-q)(1+q+q²)), and c_{s-2γ}^{-1} ≤ 2/(s-2γ) ≤ 3/s (needs s ≥ 6γ and s - 2γ ≤ 1). One factor of c_{s-2γ} then cancels against the poles, giving

c_{2s} · Σ ≤ 108 γ² (1-q)^{-2} + 54 γ² h² + 27 E⁴γ²|log γ|⁴ ≤ 972 γ² s^{-2} + 54 γ² h² + 27 E⁴γ²|log γ|⁴,

and max{972, 54, 27} ≤ 1024. The stated constant 1024 is an absolute numeral chosen for roundness; the derivation supports 972.

Only s ≥ 6γ is used. The binder is stated at the source window 8γ ≤ s (tex s ∈ [8γ, 1]), which is what every caller has.

Carriers and consumer fit

• The outer weight is spelled Real.rpow (3 : ℝ) (-s * (j : ℝ)), byte-for-byte the spelling of breakdownLegSum (Provider/Localization/Breakdown.lean), whose reindexing convention `j = m
  • l ∈ ℕ, scale m - (j: ℤ)`, this module adopts.
• c_{2s} is Book.Ch02.geometricDiscount s 2 (CoarseGraining, Homogenization/Book/Ch02/MultiscaleEllipticity.lean), the carrier Breakdown.lean already identifies with the manuscript's c_{2s}. Its unfolding is geometricDiscount_two_eq.
• The main consumer entry point is localization_remainder_series_le_of_termwise: it takes an arbitrary nonnegative per-scale remainder f dominated termwise by C * switchRemainder γ E h j and returns the collapsed amplitude at 1024 * C. Its Summable obligation is discharged internally, so callers owe none.

Main results

The 8 privates are rpow_three, geometricDiscount_two_le_three_mul_shift, inv_one_sub_shift_le, sq_succ_le_two_mul_choose, weight_reindex, hasSum_envelope, weighted_switchRemainder_le, collapse_core. The 10 publics, in file order:

• geometricDiscount_two_eq --- the c_{2s} = 1 - 3^{-2s} normal form.
• geometricDiscount_two_nonneg, geometricDiscount_two_le_four_mul --- q = 2 wrappers of upstream CoarseGraining publics (see the retraction above), not new results.
• switchRemainder, switchRemainder_nonneg --- the corrected per-cube remainder envelope.
• An identity, not an estimate.
• summable_weighted_switchRemainder --- summability of the weighted family.
• localization_remainder_series_le --- the full remainder collapse.

Import closure and layering

A consumer of this module no longer gets Breakdown transitively and must

The normalization c_{2s}

theorem Algsuperdiff.Section3.Provider.Localization.geometricDiscount_two_eq (s : ℝ) : HCPolySupport.Book.Ch02.geometricDiscount s 2 = 1 - 3 ^ (-(2 * s))

The manuscript's c_{2s} = 1 - 3^{-2s} is Book.Ch02.geometricDiscount s 2.

theorem Algsuperdiff.Section3.Provider.Localization.geometricDiscount_two_nonneg {s : ℝ} (hs : 0 ≤ s) : 0 ≤ HCPolySupport.Book.Ch02.geometricDiscount s 2

c_{2s} is nonnegative for s ≥ 0. A q = 2 specialization of the upstream public Book.Ch02.book_geometricDiscount_nonneg; kept only as the normal form the collapse reads.

theorem Algsuperdiff.Section3.Provider.Localization.geometricDiscount_two_le_four_mul {s : ℝ} (hs : 0 ≤ s) : HCPolySupport.Book.Ch02.geometricDiscount s 2 ≤ 4 * s

c_{2s} = 1 - 3^{-2s} ≤ 4 s. A q = 2 specialization of the upstream public Book.Ch02.geometricDiscount_le_two_mul (c_{sq} ≤ 2 s q), which is strictly more general; kept only as the normal form the collapse reads. Only 0 ≤ s is needed.

The corrected per-cube remainder

noncomputable def Algsuperdiff.Section3.Provider.Localization.switchRemainder (gam E : ℝ) (h j : ℕ) : ℝ

The corrected per-cube remainder of the localization σ-switch, at gap Δ = j + h (j = m - l):

(min{γ²Δ², 1} + E⁴γ²|log γ|⁴) · 3^{2γΔ}.

The 3^{2γΔ} factor multiplies both summands: the input e.switchtheshoms.betterer.again carries an uncancelled 3^{γΔ}, and the e.shaking.lambda remainder squares it.

Equations

• Algsuperdiff.Section3.Provider.Localization.switchRemainder gam E h j = (min (gam ^ 2 * (↑j + ↑h) ^ 2) 1 + E ^ 4 * gam ^ 2 * |Real.log gam| ^ 4) * 3 ^ (2 * gam * (↑j + ↑h))

theorem Algsuperdiff.Section3.Provider.Localization.switchRemainder_nonneg (gam E : ℝ) (h j : ℕ) : 0 ≤ switchRemainder gam E h j

The cross-file seam bridge

Cs Cev min 1 (γ²Δ²) 3^(2*(γ*Δ)) + Cs Cev (E⁴(γ²|log γ|⁴)) 3^(2*(γ*Δ))

distributed, with min 1 (·) (the argument order of the proved shom_continuity display) and Δ = (m:ℝ) - (n:ℝ) at m n : ℤ, whereas switchRemainder is factored, with min (·) 1 (the order the tex carries) and (j:ℝ) + (h:ℝ) at j h : ℕ. The two are equal, not merely comparable — no massaging, no loss, no absorbed constant — and the whole glue is min_comm plus one ring normalization of the rpow exponent (2*(γ*Δ) is not defeq to 2*γ*Δ over ℝ) plus push_cast for the ℤ → ℝ reindex at `n:= m

• j - h`.

C := Cs * Cev then threads through localization_remainder_series_le_of_termwise by plain distributivity, since the two summands factor exactly.

theorem Algsuperdiff.Section3.Provider.Localization.switchRemainder_eq_of_gap (Cs Cev gam Eval : ℝ) (h j : ℕ) : Cs * Cev * min 1 (gam ^ 2 * (↑j + ↑h) ^ 2) * 3 ^ (2 * (gam * (↑j + ↑h))) + Cs * Cev * (Eval ^ 4 * (gam ^ 2 * |Real.log gam| ^ 4)) * 3 ^ (2 * (gam * (↑j + ↑h))) = Cs * Cev * switchRemainder gam Eval h j

The seam bridge, at the gap Δ = j + h. The distributed two-summand remainder of SwitchNormalization.shom_switch equals (Cs * Cev) times the factored switchRemainder of this module. An identity, not an estimate.

theorem Algsuperdiff.Section3.Provider.Localization.switchRemainder_eq_of_int_gap (Cs Cev gam Eval : ℝ) (m : ℤ) (h j : ℕ) : Cs * Cev * min 1 (gam ^ 2 * (↑m - ↑(m - ↑j - ↑h)) ^ 2) * 3 ^ (2 * (gam * (↑m - ↑(m - ↑j - ↑h)))) + Cs * Cev * (Eval ^ 4 * (gam ^ 2 * |Real.log gam| ^ 4)) * 3 ^ (2 * (gam * (↑m - ↑(m - ↑j - ↑h)))) = Cs * Cev * switchRemainder gam Eval h j

The seam bridge at the integer scales, n := m - j - h. The ℤ → ℝ cast the assembly owes, (m:ℝ) - (n:ℝ) = (j:ℝ) + (h:ℝ), discharged inside the identity: this is the form SwitchNormalization.shom_switch is instantiated at (m the working scale, n = l - h the deep one, j = m - l).

Reindexing and the polynomial-geometric envelope

The collapse

theorem Algsuperdiff.Section3.Provider.Localization.summable_weighted_switchRemainder {s gam E : ℝ} {h : ℕ} (hgam : 0 < gam) (hsgam : 8 * gam ≤ s) (hs1 : s ≤ 1) (hgh : gam * ↑h ≤ 1) : Summable fun (j : ℕ) => Real.rpow 3 (-s * ↑j) * switchRemainder gam E h j

The weighted family of corrected per-cube remainders is summable.

theorem Algsuperdiff.Section3.Provider.Localization.localization_remainder_series_le {s gam E : ℝ} {h : ℕ} (hgam : 0 < gam) (hsgam : 8 * gam ≤ s) (hs1 : s ≤ 1) (hgh : gam * ↑h ≤ 1) : HCPolySupport.Book.Ch02.geometricDiscount s 2 * ∑' (j : ℕ), Real.rpow 3 (-s * ↑j) * switchRemainder gam E h j ≤ 1024 * gam ^ 2 * (↑h ^ 2 + (s ^ 2)⁻¹ + E ^ 4 * |Real.log gam| ^ 4)

The remainder collapse of l.localization.mathcalE. For γ > 0, s ∈ [8γ, 1] and h ∈ ℕ with γ h ≤ 1,

c_{2s} Σ_{j ≥ 0} 3^{-sj} (min{γ²(j+h)²,1} + E⁴γ²|log γ|⁴) 3^{2γ(j+h)} ≤ 1024 γ² (h² + s^{-2} + E⁴|log γ|⁴),

at j = m - l. The constant is absolute.

theorem Algsuperdiff.Section3.Provider.Localization.localization_remainder_series_le_of_termwise {s gam E C : ℝ} {h : ℕ} {f : ℕ → ℝ} (hgam : 0 < gam) (hsgam : 8 * gam ≤ s) (hs1 : s ≤ 1) (hgh : gam * ↑h ≤ 1) (hC : 0 ≤ C) (hf0 : ∀ (j : ℕ), 0 ≤ f j) (hf : ∀ (j : ℕ), f j ≤ C * switchRemainder gam E h j) : HCPolySupport.Book.Ch02.geometricDiscount s 2 * ∑' (j : ℕ), Real.rpow 3 (-s * ↑j) * f j ≤ 1024 * C * gam ^ 2 * (↑h ^ 2 + (s ^ 2)⁻¹ + E ^ 4 * |Real.log gam| ^ 4)

The consumer entry point. Any nonnegative per-scale remainder family f dominated termwise by C · the corrected per-cube remainder collapses to the collapsed amplitude at 1024 C. The summability of the weighted family is discharged internally, so callers owe no Summable obligation.