Scalar bookkeeping for §2.2. The flow and interpolation lemmas below are algebraic consequences of scalar estimates, not proofs of PDE/ODE estimates.

theorem AVenhance.Infra.Construction.epsilon_le_one {β : ℝ} {Λ m : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) : epsilon β Λ m ≤ 1

length scales lie in (0,1].

theorem AVenhance.Infra.Construction.sum_geometric_le {r : ℝ} (hr : 0 ≤ r) (hr' : r < 1) (n : ℕ) : ∑ j ∈ Finset.range n, r ^ j ≤ (1 - r)⁻¹

Finite geometric sums are bounded by the full convergent geometric series.

theorem AVenhance.Infra.Construction.sum_le_last_mul_geometric (u : ℕ → ℝ) {r : ℝ} (hr : 0 ≤ r) (hu : ∀ (j : ℕ), u j ≤ r * u (j + 1)) (m : ℕ) : ∑ j ∈ Finset.range (m + 1), u j ≤ u m * ∑ j ∈ Finset.range (m + 1), r ^ j

Backward geometric summation for increasing amplitudes.

theorem AVenhance.Infra.Construction.a_backward_step {β : ℝ} {Λ j : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) : a β Λ j ≤ ↑Λ ^ (β - 2) * a β Λ (j + 1)

Minimal separation reverses for the negative amplitude exponent.

theorem AVenhance.Infra.Construction.a_sum_bounds {β : ℝ} {Λ : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) (m : ℕ) : ∑ j ∈ Finset.range (m + 1), a β Λ j ≤ a β Λ m * ∑ j ∈ Finset.range (m + 1), (↑Λ ^ (β - 2)) ^ j ∧ ∑ j ∈ Finset.range (m + 1), a β Λ j ≤ a β Λ m / (1 - ↑Λ ^ (β - 2))

The geometric-sum step in e.Mmbound for the actual amplitudes.

theorem AVenhance.Infra.Construction.M_numeric_closure : (2 ^ 8 + 2 ^ 18) / (1 - 2 ^ (-(14 / 3))) ≤ 2 ^ 19

The scalar numerical closure in source lines 1723–1730.

theorem AVenhance.Infra.Construction.amplitude_ratio_bound {β : ℝ} {Λ : ℕ} (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) : ↑Λ ^ (β - 2) ≤ 2 ^ (-(14 / 3))

The exact comparison with the ratio printed in e.Mmbound.

theorem AVenhance.Infra.Construction.a_sum_closure {β : ℝ} {Λ : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) (m : ℕ) : (2 ^ 8 + 2 ^ 18) * ∑ j ∈ Finset.range (m + 1), a β Λ j ≤ 2 ^ 19 * a β Λ m

The final amplitude-sum closure, with no auxiliary recurrence assumptions.

theorem AVenhance.Infra.Construction.tauPP_inverse_amplitude_bound {β : ℝ} {Λ m : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) (hm : 1 ≤ m) : tauPP β Λ m ≤ 2 ^ (-25) * (a β Λ (m - 1))⁻¹ * epsilon β Λ (m - 1) ^ delta β

Corrected upper bound, in inverse-amplitude form (stronger than 2⁻²⁴).

theorem AVenhance.Infra.Construction.inverse_amplitude_window {A M E : ℝ} (hA : 0 < A) (hM : 0 < M) (hE : E ≤ 1) (hbound : M ≤ 2 ^ 19 * A) : 2 ^ (-24) * A⁻¹ * E ≤ 2 ^ (-5) * M⁻¹

Abstract inverse-amplitude conversion used to close the flow time window.

theorem AVenhance.Infra.Construction.tauPP_induction_window {β M : ℝ} {Λ m : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) (hm : 1 ≤ m) (hM : 0 < M) (hbound : M ≤ 2 ^ 19 * a β Λ (m - 1)) : tauPP β Λ m ≤ 2 ^ (-24) * (a β Λ (m - 1))⁻¹ * epsilon β Λ (m - 1) ^ delta β ∧ tauPP β Λ m ≤ 2 ^ (-5) * M⁻¹

The actual time scale satisfies the inductive time-window condition.

theorem AVenhance.Infra.Construction.epsilon_power_sum {β p : ℝ} {Λ : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) (hp : 0 < p) (m : ℕ) : ∑ j ∈ Finset.range (m + 1), epsilon β Λ j ^ p ≤ (1 - ↑Λ ^ (-p))⁻¹

Forward scale summation for a positive exponent.

theorem AVenhance.Infra.Construction.telescoping_zero {β : ℝ} {Λ : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) (m : ℕ) : 10 * ∑ j ∈ Finset.range (m + 1), epsilon β Λ j ^ β ≤ 11

Zeroth-order telescoping scalar estimate, source 1805–1818.

theorem AVenhance.Infra.Construction.four_le_log_lambda {Λ : ℕ} (hΛ : 2 ^ 7 ≤ Λ) : 4 ≤ Real.log ↑Λ

Lambda has logarithm at least four, uniformly over the allowed range.

theorem AVenhance.Infra.Construction.first_order_denominator {β : ℝ} {Λ : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) : 5 / 3 * (β - 1) ≤ 1 - ↑Λ ^ (-(β - 1))

The geometric denominator controlling the first-order telescoping sum.

theorem AVenhance.Infra.Construction.telescoping_one {β : ℝ} {Λ : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) (m : ℕ) : 5 * epsilon β Λ m * ∑ j ∈ Finset.range (m + 1), epsilon β Λ j ^ (β - 1) ≤ 3 / (β - 1) * epsilon β Λ m

First-order telescoping scalar estimate, source 1805–1818.

theorem AVenhance.Infra.Construction.epsilon_beta_div {E β : ℝ} (hE : 0 < E) : E ^ β / E = E ^ (β - 1)

Real-power identity translating the interpolation estimate to epsilon.

theorem AVenhance.Infra.Construction.radius_step_algebra {E F R : ℝ} (hE : 0 < E) (hR : 0 ≤ R) (hsep : F ≤ E / 128) (hprev : E * R ≤ 5 / 4) : F * (9 / 4 * R + 128 * E⁻¹) ≤ 5 / 4

Scalar closure for the normalized radius recurrence.

theorem AVenhance.Infra.Construction.radius_recurrence_scaled {β : ℝ} {Λ : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) (R : ℕ → ℝ) (hR₀ : R 0 = 1) (hR : ∀ (j : ℕ), R (j + 1) = 9 / 4 * R j + 2 ^ 7 * (epsilon β Λ (j + 1))⁻¹) (m : ℕ) : epsilon β Λ (m + 1) * R m ≤ 5 / 4

The 5/4 normalized-radius bound for the recurrence in source 1683.

theorem AVenhance.Infra.Construction.radius_recurrence_bound {β : ℝ} {Λ m : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) (R : ℕ → ℝ) (hR₀ : R 0 = 1) (hR : ∀ (j : ℕ), R (j + 1) = 9 / 4 * R j + 2 ^ 7 * (epsilon β Λ (j + 1))⁻¹) (hm : 1 ≤ m) : R m ≤ (3 + 2 ^ 7) * (epsilon β Λ m)⁻¹

e.Rmbound: radius bounded by 131 epsilon⁻¹, directly from its recurrence.

theorem AVenhance.Infra.Construction.amplitude_recurrence_sum {β : ℝ} {Λ : ℕ} (M : ℕ → ℝ) (hM₀ : M 0 ≤ 2 ^ 8 + 2 ^ 18) (hstep : ∀ (j : ℕ), M (j + 1) ≤ M j + (2 ^ 8 + 2 ^ 18) * a β Λ (j + 1)) (m : ℕ) : M m ≤ (2 ^ 8 + 2 ^ 18) * ∑ j ∈ Finset.range (m + 1), a β Λ j

Summing the simplified scalar M recurrence.

theorem AVenhance.Infra.Construction.amplitude_recurrence_bound {β : ℝ} {Λ : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) (M : ℕ → ℝ) (hM₀ : M 0 ≤ 2 ^ 8 + 2 ^ 18) (hstep : ∀ (j : ℕ), M (j + 1) ≤ M j + (2 ^ 8 + 2 ^ 18) * a β Λ (j + 1)) (m : ℕ) : M m ≤ 2 ^ 19 * a β Λ m

e.Mmbound from the simplified recurrence, including its initial value.

theorem AVenhance.Infra.Construction.amplitude_step_algebra {A E R : ℝ} (hA : 0 ≤ A) (hER : 0 ≤ E * R) (hbound : E * R ≤ 5 / 4) : 2 ^ 7 * A * E ^ 2 * R ^ 2 + 2 ^ 18 * A ≤ (2 ^ 8 + 2 ^ 18) * A

Simplification of the full M increment using the normalized-radius bound.

theorem AVenhance.Infra.Construction.full_amplitude_recurrence_bound {β : ℝ} {Λ : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) (R M : ℕ → ℝ) (hR₀ : R 0 = 1) (hM₀ : M 0 = 1) (hR : ∀ (j : ℕ), R (j + 1) = 9 / 4 * R j + 2 ^ 7 * (epsilon β Λ (j + 1))⁻¹) (hM : ∀ (j : ℕ), M (j + 1) = M j + 2 ^ 7 * a β Λ (j + 1) * epsilon β Λ (j + 1) ^ 2 * R j ^ 2 + 2 ^ 18 * a β Λ (j + 1)) (m : ℕ) : M m ≤ 2 ^ 19 * a β Λ m

Full scalar recurrence closure for the source's M and R sequences.