Scalar bridges for §4. Diffusivity results named conditional take the applicable diffusivity-recursion conclusion explicitly. No draft theorem module is imported. The top index never acquires an interior two-sided bound.

theorem AVenhance.Infra.Section4.amplitude_time_power {β E p : ℝ} (hE : 0 < E) : E ^ (β - 2) * E ^ (2 - β + p) = E ^ p

Multiplication by the preceding amplitude cancels the time-scale exponent.

theorem AVenhance.Infra.Section4.time_cell_factor_bounds {β : ℝ} {Λ m : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) : 4 * epsilon β Λ (m - 1) ^ (-delta β) ≤ Ingredients.tauCellFactor β Λ m ∧ Ingredients.tauCellFactor β Λ m ≤ 9 * epsilon β Λ (m - 1) ^ (-delta β)

Uniform bounds for the integer time-cell factor, with ceilings retained.

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

a_(m−1) τ''_m ≍ ε_(m−1)^(2δ), with the corrected constants.

theorem AVenhance.Infra.Section4.amplitude_tau_bounds {β : ℝ} {Λ m : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) (hm : 1 ≤ m) : 2 ^ (-33) * epsilon β Λ (m - 1) ^ (4 * delta β) ≤ a β Λ (m - 1) * tau β Λ m ∧ a β Λ (m - 1) * tau β Λ m ≤ 2 ^ (-28) * epsilon β Λ (m - 1) ^ (4 * delta β)

a_(m−1) τ_m ≍ ε_(m−1)^(4δ).

theorem AVenhance.Infra.Section4.time_ratios_exact {β : ℝ} {Λ m : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) (hm : 1 ≤ m) : tauP β Λ m / tau β Λ m = Ingredients.tauCellFactor β Λ m ∧ tau β Λ m / tauP β Λ m = (Ingredients.tauCellFactor β Λ m)⁻¹

The two time-scale ratios are exactly reciprocal cell factors.

theorem AVenhance.Infra.Section4.time_ratio_bounds {β : ℝ} {Λ m : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) (hm : 1 ≤ m) : 1 / 9 * epsilon β Λ (m - 1) ^ delta β ≤ tau β Λ m / tauP β Λ m ∧ tau β Λ m / tauP β Λ m ≤ 1 / 4 * epsilon β Λ (m - 1) ^ delta β

The separated fast times satisfy τ/τ' ≍ ε^δ.

theorem AVenhance.Infra.Section4.amplitude_tauP_bounds {β : ℝ} {Λ m : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) (hm : 1 ≤ m) : 2 ^ (-26) / 9 * epsilon β Λ (m - 1) ^ (3 * delta β) ≤ a β Λ (m - 1) * tauP β Λ m ∧ a β Λ (m - 1) * tauP β Λ m ≤ 2 ^ (-27) * epsilon β Λ (m - 1) ^ (3 * delta β)

The intermediate time scale satisfies a τ' ≍ ε^(3δ); the printed equality is approximate.

theorem AVenhance.Infra.Section4.amplitude_le_inverse_tauP {β : ℝ} {Λ m : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) (hm : 1 ≤ m) : a β Λ (m - 1) ≤ (tauP β Λ m)⁻¹

The slow amplitude is bounded by the inverse intermediate time scale.

noncomputable def AVenhance.Infra.Section4.smallnessBudget (C₁ C₂ C₃ : ℝ) : ℝ

Explicit budget for all three smallness bridges, independent of m and Lambda.

Equations

• AVenhance.Infra.Section4.smallnessBudget C₁ C₂ C₃ = 1 + 4 * C₁ ^ 2 + 2 * C₂ + (320 / 9 * C₃ * (1 + C₂)) ^ 2

theorem AVenhance.Infra.Section4.linear_smallness_of_square {t C D : ℝ} (ht : 0 ≤ t) (hC : 0 ≤ C) (hD : 0 < D) (hbudget : 4 * C ^ 2 ≤ D) (hsmall : t ^ 2 ≤ D⁻¹) : C * t ≤ 1 / 2

Pure algebra: a squared smallness budget controls a linear loss.

theorem AVenhance.Infra.Section4.power_smallness_of_threshold {E p C η : ℝ} (hE : 0 ≤ E) (hp : 0 < p) (hC : 0 < C) (hη : 0 ≤ η) (hsmall : E ≤ (η / C) ^ p⁻¹) : C * E ^ p ≤ η

The explicit power threshold for any desired coefficient and tolerance.

theorem AVenhance.Infra.Section4.section4_exponent_budgets {β : ℝ} (hβ : 1 < β) (hβ' : β < 4 / 3) : 4 * delta β ≤ gamma β ∧ 0 < q β - 1 - gamma β / 2 ∧ 8 * delta β + 4 * (q β - 1) * (β + gamma β) ≤ delta β * ↑(Nstar β)

The gamma and derivative budgets needed by Section 4, reusing the numeric layer.

theorem AVenhance.Infra.Section4.condition_of_exprat_upper {E K T r : ℝ} (hK : 0 < K) (hT : 0 < T) (hupper : E ^ 2 / (K * T) ≤ r) (hsmall : r ≤ 1 / 2) : E ^ 2 ≤ 1 / 2 * K * T

The algebraic e.condition bridge; only an upper exprat bound is used.

theorem AVenhance.Infra.Section4.epsilon_tendsto_zero {β : ℝ} {Λ : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) : Filter.Tendsto (epsilon β Λ) Filter.atTop (nhdsWithin 0 (Set.Ioi 0))

The epsilon scales tend to zero through positive values.