FlowArithmetic

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

Deterministic scalar arithmetic for the diffusivity flow

This module is deterministic scalar-arithmetic infrastructure for the Section 3.4 diffusivity-propagation assembly. It contains only inequalities between real numbers: the two logarithmic decay estimates that convert a |log γ| inflation into a γ-power gain, the elementary square-root power comparison, and the two-sided squeeze produced by a small relative error.

Every hypothesis of every statement below is an explicit input binder chosen for the arithmetic at hand; none of them is a source premise of a frozen theorem, and no model, probability space, or analytic producer is referenced.

Main statements

• sqrt_mul_sq_abs_log_le: √γ |log γ|² ≤ 16 on (0, 1].
• mul_sq_abs_log_le: γ |log γ|² ≤ 16 √γ on (0, 1].
• sqrt_mul_abs_log_le: √γ |log γ| ≤ 4 √(√γ) on (0, 1].
• sqrt_le_inv_pow_five: γ ≤ (E⁻¹)¹⁰ gives √γ ≤ (E⁻¹)⁵.
• sq_sandwich_of_relative_error: |x − √P| ≤ θ x with θ ≤ 1/4 gives P/2 ≤ x² ≤ 2P.

The logarithmic decay estimates

theorem Algsuperdiff.Section3.Provider.Diffusivity.sqrt_mul_sq_abs_log_le {gamma : ℝ} (hgamma : 0 < gamma) (hgamma1 : gamma ≤ 1) : √gamma * |Real.log gamma| ^ 2 ≤ 16

√γ |log γ|² ≤ 16 for 0 < γ ≤ 1.

The constant 16 is the honest one: writing u = √(√γ) the bound |log γ| ≤ 4 u⁻¹ gives √γ |log γ|² ≤ u² · 16 u⁻² = 16.

theorem Algsuperdiff.Section3.Provider.Diffusivity.mul_sq_abs_log_le {gamma : ℝ} (hgamma : 0 < gamma) (hgamma1 : gamma ≤ 1) : gamma * |Real.log gamma| ^ 2 ≤ 16 * √gamma

γ |log γ|² ≤ 16 √γ for 0 < γ ≤ 1: the previous bound multiplied by √γ. This is the shape consumed by the γ-threshold arithmetic, where the factor √γ is the one later traded against a power of E⁻¹.

theorem Algsuperdiff.Section3.Provider.Diffusivity.sqrt_mul_abs_log_le {gamma : ℝ} (hgamma : 0 < gamma) (hgamma1 : gamma ≤ 1) : √gamma * |Real.log gamma| ≤ 4 * √√gamma

√γ |log γ| ≤ 4 √(√γ) for 0 < γ ≤ 1.

This is the form in which the amplitude √γ |log γ| is absorbed: the residual √(√γ) is a quarter power of γ and is later traded against E⁻².

Square roots of inverse powers

theorem Algsuperdiff.Section3.Provider.Diffusivity.sqrt_le_inv_pow_five {E gamma : ℝ} (hE : 0 < E) (hgammaE : gamma ≤ E⁻¹ ^ 10) : √gamma ≤ E⁻¹ ^ 5

From γ ≤ (E⁻¹)¹⁰ and 0 < E, √γ ≤ (E⁻¹)⁵.

The two-sided squeeze from a small relative error

theorem Algsuperdiff.Section3.Provider.Diffusivity.sq_sandwich_of_relative_error {x P theta : ℝ} (hx : 0 < x) (hP : 0 < P) (htheta : 0 ≤ theta) (htheta' : theta ≤ 1 / 4) (hdev : |x - √P| ≤ theta * x) : P / 2 ≤ x ^ 2 ∧ x ^ 2 ≤ 2 * P

Squared sandwich from a relative error. If x > 0, P > 0, and x deviates from √P by at most θ x with 0 ≤ θ ≤ 1/4, then x² and P agree within a factor 2.

The numerology is exactly (1 − θ)² ≥ 9/16 and (1 + θ)² ≤ 25/16 < 2; both slack factors 16/9 and 25/16 are below 2, so the stated constants are honest with room to spare.