Normalized coordinates for the auxiliary diffusivity recurrence.

theorem AVenhance.Infra.Section3.q_gamma_balance {β : ℝ} (hβ : 1 < β) (hβ' : β < 4 / 3) : q β * (β - gamma β) = β + gamma β

The exponents in the normalized recurrence satisfy the balance used in the source's scale conversion.

theorem AVenhance.Infra.Section3.rpow_ratio_control {e x r A : ℝ} (he : 0 ≤ e) (he128 : e ≤ 1 / 128) (hA : 0 ≤ A) (hlo : 1 - 10 * e ≤ x) (hhi : x ≤ 1 + A * e) (hr : 0 < r) (hr2 : r ≤ 2) : x ^ r ≤ 1 + (2 * A + A ^ 2 / 128) * e ∧ (x ^ r)⁻¹ ≤ 1 + 50 * e

A supergeometric ratio raised to the exponent β−γ stays within a linear error. The proof keeps the real-power estimates separate from the polynomial inequalities.

theorem AVenhance.Infra.Section3.kappaPrime_ratio_factor_bounds {β : ℝ} {Λ m : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) (hm : 1 ≤ m) : have R := (epsilon β Λ (m + 1) / epsilon β Λ m ^ q β) ^ (β - gamma β); R ≤ 1 + (2 * Ingredients.supergeoConstant β + Ingredients.supergeoConstant β ^ 2 / 128) * epsilon β Λ m ∧ R⁻¹ ≤ 1 + 50 * epsilon β Λ m

The corrected supergeometric estimate controls the exact normalized recurrence factor by 1 + C(β) ε_m. This uses exponent β−γ; the source's display at e.bound.some.stuff writes β there, while the exact balance is q(β−γ)=β+γ.

noncomputable def AVenhance.Infra.Section3.kappaPrimeNormalized (β : ℝ) (Λ : ℕ) (κ : ℝ) (m d : ℕ) : ℝ

The auxiliary recurrence in coordinates normalized by ε_m^(β+γ). The forcing term is 9/80; scaling the diffusivity by sqrt(80/9) would instead make that term one.

Equations

• AVenhance.Infra.Section3.kappaPrimeNormalized β Λ κ m d = AVenhance.Infra.Section3.kappaPrimeAt β Λ κ m d / AVenhance.epsilon β Λ m ^ (β + AVenhance.gamma β)

theorem AVenhance.Infra.Section3.kappaPrimeNormalized_step {β : ℝ} {Λ : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) {κ : ℝ} (hκ : 0 < κ) (m d : ℕ) : kappaPrimeNormalized β Λ κ m (d + 1) = (epsilon β Λ (m + 1) / epsilon β Λ m ^ q β) ^ (β - gamma β) * (epsilon β Λ (m + 1) ^ (2 * gamma β) * kappaPrimeNormalized β Λ κ (m + 1) d + 9 / 80 / kappaPrimeNormalized β Λ κ (m + 1) d)

Exact one-step normalized recurrence. It uses exponent β−γ on the supergeometric ratio, as follows from q(β−γ)=β+γ.

noncomputable def AVenhance.Infra.Section3.kappaPrimeNormalizedSize (β : ℝ) (Λ : ℕ) (κ : ℝ) (m d : ℕ) : ℝ

A reciprocal-symmetric size that is invariant under the limiting map s ↦ (9/80)/s.

Equations

• AVenhance.Infra.Section3.kappaPrimeNormalizedSize β Λ κ m d = max (AVenhance.Infra.Section3.kappaPrimeNormalized β Λ κ m d) (9 / 80 / AVenhance.Infra.Section3.kappaPrimeNormalized β Λ κ m d)

noncomputable def AVenhance.Infra.Section3.kappaPrimeNormalizedStepFactor (β : ℝ) (Λ m : ℕ) : ℝ

The multiplicative factor in one step of the normalized size estimate.

Equations

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

theorem AVenhance.Infra.Section3.kappaPrimeNormalized_pos {β : ℝ} {Λ : ℕ} {κ : ℝ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) (hκ : 0 < κ) (m d : ℕ) : 0 < kappaPrimeNormalized β Λ κ m d

theorem AVenhance.Infra.Section3.kappaPrimeNormalizedSize_step {β : ℝ} {Λ : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) {κ : ℝ} (hκ : 0 < κ) (m d : ℕ) : kappaPrimeNormalizedSize β Λ κ m (d + 1) ≤ max ((epsilon β Λ (m + 1) / epsilon β Λ m ^ q β) ^ (β - gamma β)) ((epsilon β Λ (m + 1) / epsilon β Λ m ^ q β) ^ (β - gamma β))⁻¹ * (1 + epsilon β Λ (m + 1) ^ (2 * gamma β)) * kappaPrimeNormalizedSize β Λ κ (m + 1) d

One normalized recurrence step grows the reciprocal-symmetric size by the scale-ratio factor and an ε^(2γ) perturbation.