HomSeamBudgetArith

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

The budget: the two |log γ| costs multiply to exactly ONE |log γ|

What this file supplies

The corrected statement enlarges the moment display of Theorem B from |log γ|² to |log γ|³. It assigns the ONE new log to the product of the two machine-pinned costs of realizing Step 3 at the fixed exponent p = 4d:

  D3   = coarseGrainingGeomFactor (4d) (s/4)          ≈ |log γ|^{1/(4d)}
  CA   = (1 + (s·p')⁻¹)^{1/p'}                        ≈ |log γ|^{1-1/(4d)}

This file proves, over abstract reals and with NO model in sight, that the product is at most 2·|log γ| on the printed gate 4 ≤ |log γ| — i.e. that the one extra log of the frozen display is enough, with a numeral to spare and with NO dependence of the budget constant on d.

  coarseGrainingGeomFactor_le_one_add_inv   -- D3 ≤ (1 + (w·p)⁻¹)^{1/p}
  geomFactor_mul_farBandFactor_le_two_mul   -- the product, at conjugate (p,q)
  recut_geomBudget_le                       -- the same at the §4.5 pin p = 4d
  recut_geomBudget_le_absLog                -- and at s = homS M, on the gate

The two ≈ above are necessity records — the D3 lower bound and the far-band lower bound; this file supplies the matching UPPER bounds, which is what the budget slot consumes.

1. log 3 ≥ 1, and the elementary convexity bound it feeds

theorem Algsuperdiff.Section4.Provider.Homogenization.one_le_log_three : 1 ≤ Real.log 3

e ≤ 3, hence 1 ≤ log 3.

theorem Algsuperdiff.Section4.Provider.Homogenization.one_add_le_three_rpow {x : ℝ} (hx : 0 ≤ x) : 1 + x ≤ 3 ^ x

1 + x ≤ 3^x for x ≥ 0. exp dominates its tangent at 0 and log 3 ≥ 1.

2. The D3 upper bound

theorem Algsuperdiff.Section4.Provider.Homogenization.coarseGrainingGeomFactor_le_one_add_inv {p w : ℝ} (hp : 0 < p) (hw : 0 < w) : coarseGrainingGeomFactor p w ≤ (1 + (w * p)⁻¹) ^ (1 / p)

THE D3 FACTOR, FROM ABOVE.

coarseGrainingGeomFactor p w = (1-3^{-wp})^{-1/p} ≤ (1 + (w·p)⁻¹)^{1/p}.

This is the exact companion of the D3 necessity record: both sides behave like (wp)^{-1/p} as w·p → 0, so nothing is lost here. No gate, no γ, no d.

3. THE BUDGET: the two costs multiply to one L

theorem Algsuperdiff.Section4.Provider.Homogenization.geomFactor_mul_farBandFactor_le_two_mul {p q L w : ℝ} (hp : 1 ≤ p) (hq : 1 ≤ q) (hpq : 1 / p + 1 / q = 1) (hL : 1 ≤ L) (hw : 0 < w) (hwpL : (w * p)⁻¹ ≤ L) : coarseGrainingGeomFactor p w * (1 + (L⁻¹ * q)⁻¹) ^ (1 / q) ≤ 2 * L

THE BUDGET INEQUALITY, over abstract reals.

At a conjugate pair (p, q) (1/p + 1/q = 1) the product of

• the ℓ^p depth-aggregation energy factor coarseGrainingGeomFactor p w, and
• the dual-converse far-band factor (1 + (L⁻¹·q)⁻¹)^{1/q}

is at most 2·L, provided only that (w·p)⁻¹ ≤ L and 1 ≤ L. The two exponents 1/p and 1/q add to 1: that is the whole content — one log, not two, and the constant is the numeral 2.

4. THE BUDGET AT THE §4.5 PIN p = 4d

theorem Algsuperdiff.Section4.Provider.Homogenization.recut_geomBudget_le (d : ℕ) (hd1 : 1 ≤ d) {L : ℝ} (hL : 1 ≤ L) : coarseGrainingGeomFactor (recutExponent d hd1).exponent.toReal (L⁻¹ / 4) * (1 + (L⁻¹ * (recutExponent d hd1).conjugate.exponent.toReal)⁻¹) ^ (1 / (recutExponent d hd1).conjugate.exponent.toReal) ≤ 2 * L

THE BUDGET AT THE PIN. p = 4d, w = s/4 with s = L⁻¹, and q the Hölder conjugate of 4d: the product of the D3 energy factor and the dual-converse far-band factor is at most 2·L.

The pin's arithmetic is w·p = (L⁻¹/4)·(4d) = d/L, so (w·p)⁻¹ = L/d ≤ L as soon as 1 ≤ d. The d-dependence of the two individual factors (L^{1/(4d)} and L^{1-1/(4d)}) cancels EXACTLY: the budget constant is the numeral 2.

theorem Algsuperdiff.Section4.Provider.Homogenization.recut_geomFactor_le_two_mul (d : ℕ) (hd1 : 1 ≤ d) {L : ℝ} (hL : 1 ≤ L) : coarseGrainingGeomFactor (recutExponent d hd1).exponent.toReal (L⁻¹ / 4) ≤ 2 * L

THE D3 FACTOR ALONE IS INSIDE THE BUDGET.

At the §4.5 pin the geometric factor of the ℓ^p energy slot is at most 2·L all by itself: it is ≍ L^{1/(4d)}, and one whole log is more than enough. This discharges the factor D3 on its own, inside the frozen budget.

theorem Algsuperdiff.Section4.Provider.Homogenization.recut_geomFactor_le_absLog {d : ℕ} (hd1 : 1 ≤ d) (M : Section3.ABKModel d) (hlog : 4 ≤ |Real.log M.gamma|) : coarseGrainingGeomFactor (recutExponent d hd1).exponent.toReal (homS M / 4) ≤ 2 * |Real.log M.gamma|

D3, DISCHARGED ON THE PRINTED GATE. GEOM ≤ 2·|log γ|.

theorem Algsuperdiff.Section4.Provider.Homogenization.recut_geomBudget_le_absLog {d : ℕ} (hd1 : 1 ≤ d) (M : Section3.ABKModel d) (hlog : 4 ≤ |Real.log M.gamma|) : coarseGrainingGeomFactor (recutExponent d hd1).exponent.toReal (homS M / 4) * (1 + (homS M * (recutExponent d hd1).conjugate.exponent.toReal)⁻¹) ^ (1 / (recutExponent d hd1).conjugate.exponent.toReal) ≤ 2 * |Real.log M.gamma|

THE BUDGET ON THE PRINTED GATE, at the own order s = homS M = |log γ|⁻¹. This is the inequality the frozen display's free factor slot has to absorb, machine-checked: D3 · CA ≤ 2·|log γ|.