Fine material rate comparisons with the corrected supergeometric factor.

noncomputable def AVenhance.Infra.Section4.amnrFineScaleFactor (β : ℝ) : ℝ

The corrected factor retained in the material rate comparison.

Equations

• AVenhance.Infra.Section4.amnrFineScaleFactor β = 1 + AVenhance.Infra.Ingredients.supergeoConstant β

theorem AVenhance.Infra.Section4.amnr_epsilon_weak_supergeo {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) : epsilon β I.Λ m ≤ amnrFineScaleFactor β * epsilon β I.Λ (m - 1) ^ q β

A uniform weak supergeometric upper bound, including the base scale.

theorem AVenhance.Infra.Section4.amnr_fine_material_exponent {β : ℝ} (hβ : 1 < β) (hβ' : β < 4 / 3) : q β * (β - 2) ≤ β - 2 - 4 * delta β

The source exponent gap absorbs the fine time radius into the current amplitude. Only scalar polynomial identities enter this step.

noncomputable def AVenhance.Infra.Section4.amnrFineMaterialConstant (β : ℝ) : ℝ

A β-dependent constant, independent of the scale, for the fine rate.

Equations

• AVenhance.Infra.Section4.amnrFineMaterialConstant β = 2 ^ 33 * AVenhance.Infra.Section4.amnrFineScaleFactor β ^ (2 - β)

theorem AVenhance.Infra.Section4.amnr_inverse_tau_le_current_amplitude {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) : (tau β I.Λ m)⁻¹ ≤ amnrFineMaterialConstant β * a β I.Λ m

The actual fine cutoff rate is controlled by the current amplitude. The corrected factor is used rather than a false uniform supergeometric constant.