SecondTermArithmetic

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

Step 5's second summand: the scalar arithmetic

Everything below is abstract-real arithmetic: no model, no measure, no carrier occurs.

What is here

The four scalar facts Step 5's per-cube evaluation needs, and that the proved layer does not already carry.

1. A power against a decaying exponential. x^n e^{-x} ≤ n!, hence y^n e^{-aγ^{-1}} ≤ n!/a^n whenever 0 ≤ y ≤ γ^{-1}. This is what makes the printed q²e^{-C^{-1}γ^{-1}} of bullet (B4) and the printed q³e^{-C^{-1}γ^{-1}} of bullet (B5) bounded on the anchor's own p-range p ≤ C^{-1}γ^{-1}s (which gives q ≤ γ^{-1}): the γ-power the moment conversion spends is paid by the exponential, with no p-restriction.

2. The γ^{3/5}|log γ|² portion of bullet (B2), squared. (γ^{3/5}|log γ|²)² ≤ 160000 γ. The square is essential: γ^{3/5}|log γ|² itself is NOT O(γ), but (B2) is a squared display, and after squaring the |log γ|-power is beaten by γ^{1/5}. The scale-free ingredient is γ^{1/10}(log γ)² ≤ 400.

3. The min-square split. (min{1, a+b})² ≤ 2a + 2b² for a, b ≥ 0. Applied at a = γ(t+2), b = γ^{3/5}|log γ|² this converts bullet (B2)'s squared minimum into the linear and flat per-scale shapes of MinkowskiProviderFinal.minkowskiScaleMajorant, at both branches of the minimum at once.

Also here: (1 − 3^{γ−1})^{-1} ≤ 3 at γ ≤ 1/2, the uniformizer that turns the γ-dependent geometric constants of GradBottomLayer/GradSlotMoment into dimensional ones.

References

• ABK26, l.bounds.mathcal.E.aL, Step 4 bullets (B2)/(B4)/(B5)/(B6b), Step 5.

1. A power against a decaying exponential

theorem Algsuperdiff.Section4.Provider.BoundsEaL.pow_mul_exp_neg_le (n : ℕ) {x : ℝ} (hx : 0 ≤ x) : x ^ n * Real.exp (-x) ≤ ↑n.factorial

x^n e^{-x} ≤ n! for x ≥ 0: the single term x^n/n! of the exponential series is at most the whole series.

theorem Algsuperdiff.Section4.Provider.BoundsEaL.pow_mul_exp_neg_inv_le {a g y : ℝ} (n : ℕ) (ha : 0 < a) (hg : 0 < g) (hy0 : 0 ≤ y) (hy : y ≤ g⁻¹) : y ^ n * Real.exp (-(a * g⁻¹)) ≤ ↑n.factorial / a ^ n

The moment q-power against the printed exponential amplitude.

On the anchor's own range q ≤ γ^{-1} the printed q^n e^{-aγ^{-1}} of the Step-4 moment conversions is bounded by the absolute constant n!/a^n: NO restriction on p is used, and no γ-power is moved.

theorem Algsuperdiff.Section4.Provider.BoundsEaL.pow_mul_exp_neg_inv_le_mul {a g y : ℝ} (n : ℕ) (ha : 0 < a) (hg : 0 < g) (hy0 : 0 ≤ y) (hy : y ≤ g⁻¹) : y ^ n * Real.exp (-(a * g⁻¹)) ≤ ↑(n + 1).factorial / a ^ (n + 1) * g

The same, with one factor γ to spare.

y^n e^{-aγ^{-1}} ≤ ((n+1)!/a^{n+1}) γ on 0 ≤ y ≤ γ^{-1}. This is the form Step 5's per-scale evaluation needs: the printed exponential beats the moment q-power AND still produces the γ of the anchor's own scalar.

2. The |log γ| portion of bullet (B2)

theorem Algsuperdiff.Section4.Provider.BoundsEaL.rpow_tenth_mul_log_sq_le {g : ℝ} (hg : 0 < g) (hg1 : g ≤ 1) : g ^ (1 / 10) * Real.log g ^ 2 ≤ 400

The scale-free log bound at the exponent 1/10. γ^{1/10}(log γ)² ≤ 400 on (0,1]: the t = γ^{1/20} core, where t·t·(20 log t)² = 400 (t log t)².

theorem Algsuperdiff.Section4.Provider.BoundsEaL.gammaLogPortion_sq_le {g : ℝ} (hg : 0 < g) (hg1 : g ≤ 1) : (g ^ (3 / 5) * |Real.log g| ^ 2) ^ 2 ≤ 160000 * g

Bullet (B2)'s |log γ| portion, squared.

(γ^{3/5}|log γ|²)² ≤ 160000 γ. The square is what makes the portion O(γ): γ^{3/5}|log γ|² itself is not, and (B2) is a squared display.

theorem Algsuperdiff.Section4.Provider.BoundsEaL.add_sq_le_two_mul (x y : ℝ) : (x + y) ^ 2 ≤ 2 * x ^ 2 + 2 * y ^ 2

(x+y)² ≤ 2x² + 2y², the two-lane split of bullet (B4)'s squared majorant. Proved from (x−y)² ≥ 0 alone: no numeric tactic touches the transcendental atoms of the lanes.

3. The two squared-minimum splits

theorem Algsuperdiff.Section4.Provider.BoundsEaL.min_one_add_sq_le {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) : min 1 (a + b) ^ 2 ≤ 2 * a + 2 * b ^ 2

The min-square split. (min{1, a+b})² ≤ 2a + 2b² for a, b ≥ 0.

Both branches of the minimum are covered at once: below the cap the square of the sum is ≤ 2a² + 2b² ≤ 2a + 2b², and above it the constant 1 is already dominated by 2(a+b) − 1/2 ≥ 3/2.

theorem Algsuperdiff.Section4.Provider.BoundsEaL.one_add_min_sqrt_sq_le {a b : ℝ} (hb : 0 ≤ b) : (1 + min √a √b) ^ 2 ≤ 2 * (1 + b)

This is the additive 1 carried through the square, at the branch √b of the minimum.

4. Two gauge-weight identities

theorem Algsuperdiff.Section4.Provider.BoundsEaL.le_rpow_neg_mul_of_rpow_mul_le {y X B : ℝ} (h : 3 ^ y * X ≤ B) : X ≤ 3 ^ (-y) * B

The gauge weight, moved to the other side. A bound on 3^y X is a bound on X with the weight inverted; the development's per-scale evaluation reads the Step-4 bullets in this second form.

theorem Algsuperdiff.Section4.Provider.BoundsEaL.rpow_three_gauge_triple (a b : ℝ) : 3 ^ (-a) * (3 ^ (-b) * 3 ^ (2 * a)) = 3 ^ (a - b)

The three gauge weights of the second summand's value leg, combined. 3^{-a} · (3^{-b} · 3^{2a}) = 3^{a−b}: the two inverted weights of σ_m^{-1} and of the λ-slot against the value slot's 3^{2γm}. This is where the per-scale factor 3^{γ(m−j)} of Step 5's geometric sum comes from.

theorem Algsuperdiff.Section4.Provider.BoundsEaL.rpow_three_le_rpow_three {a b : ℝ} (hab : a ≤ b) : 3 ^ a ≤ 3 ^ b

The gauge weight is monotone in the exponent.

5. The geometric uniformizer

theorem Algsuperdiff.Section4.Provider.BoundsEaL.rpow_three_gamma_sub_one_le {g : ℝ} (hg : g ≤ 1 / 2) : Real.rpow 3 (g - 1) ≤ 3 / 5

3^{γ−1} ≤ 3/5 at γ ≤ 1/2, through √3 ≥ 5/3.

theorem Algsuperdiff.Section4.Provider.BoundsEaL.inv_one_sub_rpow_three_gamma_le {g : ℝ} (hg : g ≤ 1 / 2) : (1 - Real.rpow 3 (g - 1))⁻¹ ≤ 3

The geometric uniformizer. (1 − 3^{γ−1})^{-1} ≤ 3 at γ ≤ 1/2.

This is what turns GradBottomLayer.fullGradConst and GradSlotMoment.deepGradConst -- both of which carry the γ-dependent factor (1 − 3^{γ−1})^{-1} -- into dimensional constants, as Step 5's per-cube evaluation needs (its constant is chosen before the model).