Descent

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

Deterministic recurrence integration: adaptive descent

This file formalizes the adaptive descent and its purely ordered telescoping backbone for ABK26 l.integrate.approx.recurrence, Steps 3--4. The argument uses a single step-back strong induction, an equivalent presentation of the paper’s adaptive-chain summation.

References

• ABK26.

theorem Algsuperdiff.Section3.Provider.Diffusivity.RecurrenceIntegration.Internal.growth_side {G q δ κ : ℝ} (hG : 0 ≤ G) (hδ : 0 ≤ δ) (hκ : κ = Real.log 3 / 18) (h1mq : δ * Real.log 3 / 2 ≤ 1 - q) : 2 * κ * δ * G ≤ G * (1 - q)

Growth-flavoured one-sided drop: the G(1 − q) factorization dominates 2κδ·G once 1 − q ≥ (δ log 3)/2. Here κ = log 3 / 18.

theorem Algsuperdiff.Section3.Provider.Diffusivity.RecurrenceIntegration.Internal.plateau_side {Gn w r b : ℝ} (hGn : 0 ≤ Gn) (hb : b ≤ Gn * w) (hr : w ≤ r - 1) : b ≤ Gn * (r - 1)

Plateau-flavoured one-sided drop, outer step: if b ≤ G_n·w and w ≤ r − 1 with G_n ≥ 0, then b ≤ G_n·(r − 1).

theorem Algsuperdiff.Section3.Provider.Diffusivity.RecurrenceIntegration.Internal.plateau_product {cstar Kγ gm gn q γ a δ ν2 κ : ℝ} (hgn : gn = gm * q) (hq : 1 / 9 ≤ q) (hgm : 0 < gm) (hγ : 0 < γ) (ha : γ * δ * ν2 * cstar⁻¹ * gm⁻¹ ≤ 2 * γ * a) (hγKγ : 1 ≤ γ * Kγ) (hcstar : 0 < cstar) (hδ : 0 ≤ δ) (hν2 : 0 ≤ ν2) (hKγ : 0 ≤ Kγ) (hκ : κ = Real.log 3 / 18) : 2 * κ * δ * ν2 ≤ cstar * Kγ * gn * (2 * γ * a * Real.log 3)

Plateau-flavoured one-sided drop, inner product estimate (all opaque reals). With G_n = c⋆K_γ·g_n, g_n = g_m·q, q ≥ 1/9, the adaptive-step lower bound γδν²c⋆⁻¹g_m⁻¹ ≤ 2γa, and γK_γ ≥ 1, one has 2κδν² ≤ c⋆K_γ·g_n·(2γa·log 3) with κ = log 3 / 18.

theorem Algsuperdiff.Section3.Provider.Diffusivity.RecurrenceIntegration.Internal.quad_bound {cf μn a δ γ E : ℝ} (hμa : μn * a ≤ δ * γ⁻¹) (hμn : 0 ≤ μn) (ha : 0 ≤ a) (hδ : 0 ≤ δ) (hcf : 0 < cf) (hγ : 0 < γ) (hδ2 : δ ^ 2 * cf = E * γ) : cf * μn ^ 2 * γ * a ^ 2 ≤ E

Quadratic-term control (abstract reals). With cf = 1 + c⋆⁻²F, the adaptive step choice μ_n·a ≤ δγ⁻¹ and the constant identity δ²·cf = Eγ force the chunk's quadratic term below E: cf·μ_n²·γ·a² ≤ E.

theorem Algsuperdiff.Section3.Provider.Diffusivity.RecurrenceIntegration.Internal.small_scale_algebra {sm2 nu2 gm cstar cplus γ Kγ β : ℝ} (hnu2 : 0 < nu2) (hcstar : 0 < cstar) (hcc : cstar ≤ cplus) (hγ : 0 < γ) (hgm : 0 ≤ gm) (hlo : nu2 ≤ sm2) (hup : sm2 ≤ (1 + β) ^ 2 * nu2) (hβdef : β = nu2⁻¹ * cplus * γ⁻¹ * gm) (hβ1 : β ≤ 1) (hγ1 : 4 * γ ≤ 1) (hKγlo : γ⁻¹ ≤ Kγ) (hKγhi : Kγ ≤ γ⁻¹ + 4) : |sm2 - (nu2 + cstar * Kγ * gm)| ≤ 5 * (cplus * γ⁻¹ * gm)

Small-scale base case (abstract reals), two-constant form. From the small-scale two-sided bound ν² ≤ s_m² ≤ (1+β)²ν² with the envelope constant c⁺ (β = ν⁻²c⁺γ⁻¹3^{2γm}), β ≤ 1, 4γ ≤ 1, and γ⁻¹ ≤ K_γ ≤ γ⁻¹+4, the squared deviation against the comparator T_m built from the recurrence constant c⋆ ≤ c⁺ obeys the crude bound |s_m² − T_m| ≤ 5·c⁺γ⁻¹3^{2γm}.

This is e.small.m.is.done in division-free form. The final ≤ C₀√(Θγ)T_m shape is recovered downstream using g_m ≤ B_b.

theorem Algsuperdiff.Section3.Provider.Diffusivity.RecurrenceIntegration.Internal.rpow_ge_one_add (v : ℝ) (_hv : 0 ≤ v) : v * Real.log 3 ≤ 3 ^ v - 1

Elementary lower bound 3^v − 1 ≥ v·log 3 for v ≥ 0, from 1 + t ≤ eᵗ. Used for the plateau-flavoured drop G_n(3^{2γh} − 1).

theorem Algsuperdiff.Section3.Provider.Diffusivity.RecurrenceIntegration.Internal.one_sub_rpow_neg_ge (u : ℝ) (hu : 0 ≤ u) (hsmall : u * Real.log 3 ≤ 1) : u * Real.log 3 / 2 ≤ 1 - 3 ^ (-u)

Elementary lower bound 1 − 3^{−u} ≥ (u·log 3)/2 valid whenever 0 ≤ u·log 3 ≤ 1. Proof: with t = u log 3, eᵗ ≥ t+1 gives 3^{−u} = e^{−t} ≤ 1/(t+1), hence 1 − 3^{−u} ≥ t/(t+1) ≥ t/2. Used for the growth-flavoured drop G_m(1 − 3^{−2γh}).

theorem Algsuperdiff.Section3.Provider.Diffusivity.RecurrenceIntegration.Internal.drop_combine {κ δ nu2 G T drop : ℝ} (hB1 : 2 * κ * δ * nu2 ≤ drop) (hB2 : 2 * κ * δ * G ≤ drop) (hT : T = nu2 + G) : κ * δ * T ≤ drop

Drop combination. From the two one-sided drop bounds 2κδ·ν² ≤ drop (plateau) and 2κδ·G ≤ drop (growth), together with the comparator split T = ν² + G, derive the clean drop bound κδ·T ≤ drop. (Uses only max ≥ average: a quantity dominating both a and b dominates (a+b)/2.)

theorem Algsuperdiff.Section3.Provider.Diffusivity.RecurrenceIntegration.Internal.per_step_algebra {absval Tm Tn E γ δ R C₀ κ : ℝ} (hchunk : absval ≤ 6400 * E * γ * Tm) (hEγ : E * γ = δ * R) (hdrop : κ * δ * Tm ≤ Tm - Tn) (hRnn : 0 ≤ R) (hδnn : 0 ≤ δ) (hTmnn : 0 ≤ Tm) (hκ : 0 < κ) (hC₀κ : 6400 ≤ C₀ * κ) : absval ≤ C₀ * R * (Tm - Tn)

Per-step assembly (abstract reals). The engine of the descent's hstep: the chunk estimate absval ≤ 6400·E·γ·T_m (after folding the quadratic term ≤ E), the constant identity E·γ = δ·R, and the drop bound κδ·T_m ≤ T_m − T_n combine — provided the descent constant satisfies 6400 ≤ C₀·κ — into the one-step descent inequality absval ≤ C₀·R·(T_m − T_n) = Φ_m − Φ_n. All rpow-bearing quantities enter only as the opaque scalars absval, Tm, Tn, E, γ, δ, R.

theorem Algsuperdiff.Section3.Provider.Diffusivity.RecurrenceIntegration.Internal.geometricTerm_split (γ : ℝ) (n m : ℤ) : geometricTerm γ m = geometricTerm γ n * 3 ^ (2 * γ * (↑m - ↑n))

Geometric ratio, integer step form: 3^{2γm} = 3^{2γn}·3^{2γ(m−n)}.

theorem Algsuperdiff.Section3.Provider.Diffusivity.RecurrenceIntegration.Internal.geometricTerm_split_inv (γ : ℝ) (n m : ℤ) : geometricTerm γ n = geometricTerm γ m * 3 ^ (-(2 * γ * (↑m - ↑n)))

3^{2γn} = 3^{2γm}·3^{−2γ(m−n)}.

theorem Algsuperdiff.Section3.Provider.Diffusivity.RecurrenceIntegration.Internal.recurrenceComparator_sub_eq_cstar_mul_Kgamma {ν cstar γ : ℝ} {n m : ℤ} : recurrenceComparator ν cstar γ m - recurrenceComparator ν cstar γ n = cstar * Stream.Kgamma γ * (geometricTerm γ m - geometricTerm γ n)

Comparator difference in factored form: T_m − T_n = c⋆ K_γ (3^{2γm} − 3^{2γn}) for n ≤ m.

theorem Algsuperdiff.Section3.Provider.Diffusivity.RecurrenceIntegration.Internal.drop_bound {ν cstar γ : ℝ} (hcstar : 0 < cstar) (hγ : 0 < γ) {δ : ℝ} (hδpos : 0 < δ) (hδlog : δ * Real.log 3 ≤ 1) {n m : ℤ} (hnm : n ≤ m) (hF1 : 1 / 2 * (δ * ν ^ 2 * cstar⁻¹ * (geometricTerm γ m)⁻¹) ≤ ↑m - ↑n) (hF2 : δ ≤ 2 * γ * (↑m - ↑n)) (hF3 : 2 * γ * (↑m - ↑n) ≤ 2) : Real.log 3 / 18 * δ * recurrenceComparator ν cstar γ m ≤ recurrenceComparator ν cstar γ m - recurrenceComparator ν cstar γ n

Drop bound (Step 3 geometric heart). For a single adaptive step n = m − h (with a = m − n the real step length), the comparator drops by at least κδ·T_m with κ = log 3 / 18, provided the step obeys the three structural bounds:

• h ½·δν²c⋆⁻¹3^{−2γm} ≤ a` — the plateau lower bound on the step;
• h δ ≤ 2γa` — the growth lower bound on the step;

Proof: split T_m − T_n = c⋆K_γ(3^{2γm} − 3^{2γn}) into its growth (G_m(1 − 3^{−2γh})) and plateau (G_n(3^{2γh} − 1)) factorizations, bound each via Growth/Plateau, and fuse with drop_combine.

Floor and threshold helpers

theorem Algsuperdiff.Section3.Provider.Diffusivity.RecurrenceIntegration.Internal.floor_ge_half {x : ℝ} (hx : 2 ≤ x) : x / 2 ≤ ↑⌊x⌋

⌊x⌋ ≥ x/2 when x ≥ 2.

theorem Algsuperdiff.Section3.Provider.Diffusivity.RecurrenceIntegration.Internal.one_le_floor {x : ℝ} (hx : 2 ≤ x) : 1 ≤ ⌊x⌋

⌊x⌋ ≥ 1 when x ≥ 2.

theorem Algsuperdiff.Section3.Provider.Diffusivity.RecurrenceIntegration.Internal.geometricTerm_le_of_log_le {γ B : ℝ} (hB : 0 < B) {k : ℤ} (hk : 2 * γ * ↑k * Real.log 3 ≤ Real.log B) : geometricTerm γ k ≤ B

3^{2γk} ≤ B from 2γk·log 3 ≤ log B (for B > 0).

theorem Algsuperdiff.Section3.Provider.Diffusivity.RecurrenceIntegration.Internal.lt_geometricTerm_of_log_lt {γ B : ℝ} (hB : 0 < B) {k : ℤ} (hk : Real.log B < 2 * γ * ↑k * Real.log 3) : B < geometricTerm γ k

B < 3^{2γk} from log B < 2γk·log 3 (for B > 0).

The adaptive step size δγ⁻¹μ(m)⁻¹ and its bounds

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.RecurrenceIntegration.Internal.adaptStep (δ ν cstar γ : ℝ) (m : ℤ) : ℝ

The ideal (real) adaptive step δγ⁻¹μ(m)⁻¹, written in max form max{δν²c⋆⁻¹3^{−2γm}, δγ⁻¹}. The chosen step is its floor.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section3.Provider.Diffusivity.RecurrenceIntegration.Internal.two_le_adaptStep {ν cstar γ δ : ℝ} (hδγ2 : 2 ≤ δ * γ⁻¹) (m : ℤ) : 2 ≤ adaptStep δ ν cstar γ m

adaptStep ≥ 2 from the smallness δγ⁻¹ ≥ 2.

theorem Algsuperdiff.Section3.Provider.Diffusivity.RecurrenceIntegration.Internal.adaptStep_le_cap {ν cstar γ : ℝ} (hν : 0 < ν) (hcstar : 0 < cstar) (hγ : 0 < γ) {δ cbar : ℝ} (hδpos : 0 < δ) (hcbar : 0 < cbar) (hδcbar : δ ≤ cbar) {m : ℤ} (hgm_lb : δ * ν ^ 2 * γ * (cstar * cbar)⁻¹ ≤ geometricTerm γ m) : adaptStep δ ν cstar γ m ≤ cbar * γ⁻¹

The adaptive step never exceeds cγ⁻¹ for a capped scale c, provided δ ≤ c and 3^{2γm} ≥ δν²γ(c⋆c)⁻¹ (the mc-threshold, valid for m > mc).

Taking c = min{c⋆, 1} this yields simultaneously the chunk-range bound a ≤ c⋆γ⁻¹ (needed to invoke the two recurrence hypotheses) and the unit-range bound a ≤ γ⁻¹ (needed for 3^{2γ(m−n)} ≤ 9), with no upper bound assumed on c⋆ itself.

theorem Algsuperdiff.Section3.Provider.Diffusivity.RecurrenceIntegration.Internal.mu_mul_adaptStep_le {ν cstar γ : ℝ} (hν : 0 < ν) (hcstar : 0 < cstar) (hγ : 0 < γ) {δ : ℝ} (hδpos : 0 < δ) (m : ℤ) : min ((ν ^ 2)⁻¹ * cstar * γ⁻¹ * geometricTerm γ m) 1 * adaptStep δ ν cstar γ m ≤ δ * γ⁻¹

Key quadratic-term control: μ(m)·adaptStep ≤ δγ⁻¹, where μ(m) = min{ν⁻²c⋆γ⁻¹3^{2γm}, 1}. (In fact equality holds.)

theorem Algsuperdiff.Section3.Provider.Diffusivity.RecurrenceIntegration.Internal.bound_by_descent_le {mc m₀ : ℤ} {Φ dd : ℤ → ℝ} (nn : ℤ → ℤ) (hbase : ∀ m ≤ mc, |dd m| ≤ Φ m) (hlt : ∀ (m : ℤ), mc < m → m ≤ m₀ → nn m < m) (hstep : ∀ (m : ℤ), mc < m → m ≤ m₀ → |dd (nn m)| ≤ Φ (nn m) → |dd m - dd (nn m)| ≤ Φ m - Φ (nn m)) (m : ℤ) : m ≤ m₀ → |dd m| ≤ Φ m

Abstract descent, bounded above by m₀. Same as bound_by_descent, but the strict-descent and one-step hypotheses need only hold on (mc, m₀], and the conclusion is drawn only for m ≤ m₀. This is the form used at the call site, where the chunk estimate requires the upper endpoint to satisfy m ≤ m₀.