Section 3.3 estimates. Repeated mean-zero periodic primitives have geometric bounds, rather than the printed factorial gain (E21e).

theorem AVenhance.Infra.Section3.Approx.periodic_primitive_bound {f : ℝ → ℝ} {P B : ℝ} (hP : 0 < P) (hB : 0 ≤ B) (hf : Continuous f) (hp : Function.Periodic f P) (hz : ∫ (t : ℝ) in 0..P, f t = 0) (hb : ∀ (t : ℝ), |f t| ≤ B) (t : ℝ) : |(-∫ (s : ℝ) in 0..t, f s) + ∫ (u : ℝ) in 0..1, ∫ (s : ℝ) in 0..u, f s| ≤ 2 * P * B

theorem AVenhance.Infra.Section3.qMNR_entry_abs_le_geometric {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) {κ : ℝ} (hκ : 0 < κ) {n : ℕ} (hn : n ≤ Nstar β) (r : ℕ) (t : ℝ) (i j : Fin 2) : |I.qMNR κ m n r t i j| ≤ 2 * (2 * Real.pi ^ 2 * a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 2 / ↑n.factorial * (epsilon β I.Λ m ^ 2 / (4 * Real.pi ^ 2 * κ)) ^ n * (I.Czeta / tau β I.Λ m ^ n)) * (8 * tau β I.Λ m) ^ r

Corrected geometric bound for the actual mean-zero primitives. The factorial in the printed e.qmnr.bounds is not used.

theorem AVenhance.Infra.Section3.qMNR_entry_paper_bound {β C₀ : ℝ} (I : Ingredients β) (hcutoff : I.Czeta ≤ C₀) {m : ℕ} (hm : 1 ≤ m) {κ : ℝ} (hκ : 0 < κ) {n : ℕ} (hn : n ≤ Nstar β) (r : ℕ) (t : ℝ) (i j : Fin 2) : |I.qMNR κ m n r t i j| ≤ 4 * Real.pi ^ 2 * C₀ * (a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 2) * (epsilon β I.Λ m ^ 2 / (κ * tau β I.Λ m)) ^ n * (8 * tau β I.Λ m) ^ r

Corrected e.qmnr.bounds: a geometric gain in r, with a constant uniform in m,n,r after the cutoff constant is bounded.

theorem AVenhance.Infra.Section3.qMNR_norm_paper_bound {β C₀ : ℝ} (I : Ingredients β) (hcutoff : I.Czeta ≤ C₀) {m : ℕ} (hm : 1 ≤ m) {κ : ℝ} (hκ : 0 < κ) {n : ℕ} (hn : n ≤ Nstar β) (r : ℕ) (t : ℝ) : ‖I.qMNR κ m n r t‖ ≤ 4 * Real.pi ^ 2 * C₀ * (a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 2) * (epsilon β I.Λ m ^ 2 / (κ * tau β I.Λ m)) ^ n * (8 * tau β I.Λ m) ^ r

Supremum matrix norm version of the corrected geometric bound.

theorem AVenhance.Infra.Section3.backward_taylor_remainder {f : ℝ → ℝ} {B s t : ℝ} (k : ℕ) (hf : ContDiff ℝ (↑⊤) f) (hst : s ≤ t) (hb : ∀ (u : ℝ), |iteratedDeriv (k + 1) f u| ≤ B) : |f s - ∑ j ∈ Finset.range (k + 1), (↑j.factorial)⁻¹ * (s - t) ^ j * iteratedDeriv j f t| ≤ B * (t - s) ^ (k + 1) / ↑k.factorial

Backward Taylor remainder, with an explicit derivative bound. The extra factor (N-1)! is harmless for the fixed cutoff budget.

theorem AVenhance.Infra.Section3.Approx.taylor_remainder_exp_bound {f : ℝ → ℝ} {B ρ s t : ℝ} (k : ℕ) (hf : ContDiff ℝ (↑⊤) f) (hB : 0 ≤ B) (hρ : 0 < ρ) (hst : s ≤ t) (hb : ∀ (u : ℝ), |iteratedDeriv (k + 1) f u| ≤ B) : |f s - ∑ j ∈ Finset.range (k + 1), (↑j.factorial)⁻¹ * (s - t) ^ j * iteratedDeriv j f t| * Real.exp (ρ * (s - t)) ≤ B * ↑(k + 1) * 2 ^ (k + 1) / ρ ^ (k + 1) * Real.exp (ρ / 2 * (s - t))

theorem AVenhance.Infra.Section3.taylor_memory_remainder_bound {f h : ℝ → ℝ} {B ρ t : ℝ} (k : ℕ) (hf : ContDiff ℝ (↑⊤) f) (hB : 0 ≤ B) (hρ : 0 < ρ) (hb : ∀ (u : ℝ), |iteratedDeriv (k + 1) f u| ≤ B) (hh : ∀ (u : ℝ), |h u| ≤ 1) : |∫ (s : ℝ) in Set.Iic t, h s * (f s - ∑ j ∈ Finset.range (k + 1), (↑j.factorial)⁻¹ * (s - t) ^ j * iteratedDeriv j f t) * Real.exp (ρ * (s - t))| ≤ B * ↑(k + 1) * 2 ^ (k + 1) / ρ ^ (k + 1) * (ρ / 2)⁻¹

Exponentially weighted Taylor remainder on a half-line. The cutoff h need only be bounded; the integral estimate assumes no integrability premise.

theorem AVenhance.Infra.Section3.zetaMK_memory_remainder_bound {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (k l : ℤ) {N : ℕ} (hN : 1 ≤ N) (hbudget : N ≤ Nstar β) {ρ : ℝ} (hρ : 0 < ρ) (t : ℝ) : |∫ (s : ℝ) in Set.Iic t, I.hatZetaML m l s * (I.zetaMK m k s - ∑ j ∈ Finset.range N, (↑j.factorial)⁻¹ * (s - t) ^ j * iteratedDeriv j (I.zetaMK m k) t) * Real.exp (ρ * (s - t))| ≤ I.Czeta / tau β I.Λ m ^ N * ↑N * 2 ^ N / ρ ^ N * (ρ / 2)⁻¹

The weighted remainder for the small cutoff and a large cutoff. This is the analytic remainder needed before identifying the flux expansion.

theorem AVenhance.Infra.Section3.zetaMK_physical_memory_remainder_bound {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) {κ : ℝ} (hκ : 0 < κ) (k l : ℤ) {N : ℕ} (hN : 1 ≤ N) (hbudget : N ≤ Nstar β) (t : ℝ) : |∫ (s : ℝ) in Set.Iic t, I.hatZetaML m l s * (I.zetaMK m k s - ∑ j ∈ Finset.range N, (↑j.factorial)⁻¹ * (s - t) ^ j * iteratedDeriv j (I.zetaMK m k) t) * Real.exp (4 * Real.pi ^ 2 * κ / epsilon β I.Λ m ^ 2 * (s - t))| ≤ 2 * I.Czeta * ↑N * 2 ^ N * (epsilon β I.Λ m ^ 2 / κ) * (epsilon β I.Λ m ^ 2 / (κ * tau β I.Λ m)) ^ N

The cutoff memory remainder with the physical decay rate. This controls one Taylor remainder; it does not by itself identify the flux minus Jhat.

def AVenhance.Infra.Section3.Approx.shearAxis (k : ℤ) : Matrix (Fin 2) (Fin 2) ℝ

Coordinate-axis matrix selected by the shear index modulo four.

Equations

• AVenhance.Infra.Section3.Approx.shearAxis k = (if k % 4 = 1 then !![0, 0; 0, 1] else 0) + if k % 4 = 3 then !![1, 0; 0, 0] else 0

theorem AVenhance.Infra.Section3.Approx.other_odd_zero {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) {k l : ℤ} (hk : Odd k) (hl : Odd l) (hne : l ≠ k) {t : ℝ} (hz : I.zetaMK m k t ≠ 0) : I.zetaMK m l t = 0

theorem AVenhance.Infra.Section3.Approx.shearAxis_active {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (κ : ℝ) {k : ℤ} (hk : Odd k) {t : ℝ} (hz : I.zetaMK m k t ≠ 0) : I.flux κ m t = κ • 1 + (2 * Real.pi ^ 2 * a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 2 * I.zetaProd m k t * I.corrTime κ m k t) • shearAxis k

theorem AVenhance.Infra.Section3.flux_eq_odd_mode_sum {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (κ t : ℝ) : I.flux κ m t = κ • 1 + ∑' (k : { k : ℤ // Odd k }), (2 * Real.pi ^ 2 * a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 2 * I.zetaProd m (↑k) t * I.corrTime κ m (↑k) t) • ((if ↑k % 4 = 1 then !![0, 0; 0, 1] else 0) + if ↑k % 4 = 3 then !![1, 0; 0, 0] else 0)

The always-valid odd-mode formula for the actual flux. It applies also near the ends of even nominal time windows.

theorem AVenhance.Infra.Section3.Approx.jMN_active {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (κ : ℝ) (n : ℕ) {k : ℤ} (hk : Odd k) {t : ℝ} (hz : I.zetaMK m k t ≠ 0) : I.jMN κ m n t = (2 * Real.pi ^ 2 * a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 2 / ↑n.factorial * (epsilon β I.Λ m ^ 2 / (4 * Real.pi ^ 2 * κ)) ^ n) • (I.zetaMK m k t * iteratedDeriv n (I.zetaMK m k) t) • shearAxis k

theorem AVenhance.Infra.Section3.Approx.LMN_active {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (κ : ℝ) (n : ℕ) {k : ℤ} {t : ℝ} (hz : I.zetaMK m k t ≠ 0) : I.LMN κ m n t = I.hatZetaML m (lIdx β I.Λ m k) t * ∫ (s : ℝ) in Set.Iic t, I.hatZetaML m (lIdx β I.Λ m k) s * (4 * Real.pi ^ 2 * κ * (s - t) / epsilon β I.Λ m ^ 2) ^ n * Real.exp (4 * Real.pi ^ 2 * κ / epsilon β I.Λ m ^ 2 * (s - t))

theorem AVenhance.Infra.Section3.Approx.exp_shift_integrable {ρ : ℝ} (hρ : 0 < ρ) (t : ℝ) : MeasureTheory.IntegrableOn (fun (s : ℝ) => Real.exp (ρ * (s - t))) (Set.Iic t) MeasureTheory.volume

theorem AVenhance.Infra.Section3.Approx.polynomial_memory_integrable {h : ℝ → ℝ} (hc : Continuous h) (hh : ∀ (s : ℝ), |h s| ≤ 1) {ρ : ℝ} (hρ : 0 < ρ) (n : ℕ) (t : ℝ) : MeasureTheory.IntegrableOn (fun (s : ℝ) => h s * (s - t) ^ n * Real.exp (ρ * (s - t))) (Set.Iic t) MeasureTheory.volume

noncomputable def AVenhance.Infra.Section3.Approx.cutoffMoment {β : ℝ} (I : Ingredients β) (κ : ℝ) (m : ℕ) (l : ℤ) (n : ℕ) (t : ℝ) : ℝ

Past-time exponential moment of an enlarged cutoff, of a specified polynomial order.

Equations

• AVenhance.Infra.Section3.Approx.cutoffMoment I κ m l n t = ∫ (s : ℝ) in Set.Iic t, I.hatZetaML m l s * (s - t) ^ n * Real.exp (4 * Real.pi ^ 2 * κ / AVenhance.epsilon β I.Λ m ^ 2 * (s - t))

theorem AVenhance.Infra.Section3.Approx.cutoffMoment_integrable {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) {κ : ℝ} (hκ : 0 < κ) (l : ℤ) (n : ℕ) (t : ℝ) : MeasureTheory.IntegrableOn (fun (s : ℝ) => I.hatZetaML m l s * (s - t) ^ n * Real.exp (4 * Real.pi ^ 2 * κ / epsilon β I.Λ m ^ 2 * (s - t))) (Set.Iic t) MeasureTheory.volume

theorem AVenhance.Infra.Section3.Approx.memory_taylor_identity {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) {κ : ℝ} (hκ : 0 < κ) (k : ℤ) (N : ℕ) (t : ℝ) : I.corrTime κ m k t - ∑ n ∈ Finset.range N, (↑n.factorial)⁻¹ * iteratedDeriv n (I.zetaMK m k) t * cutoffMoment I κ m (lIdx β I.Λ m k) n t = ∫ (s : ℝ) in Set.Iic t, I.hatZetaML m (lIdx β I.Λ m k) s * (I.zetaMK m k s - ∑ n ∈ Finset.range N, (↑n.factorial)⁻¹ * (s - t) ^ n * iteratedDeriv n (I.zetaMK m k) t) * Real.exp (4 * Real.pi ^ 2 * κ / epsilon β I.Λ m ^ 2 * (s - t))

theorem AVenhance.Infra.Section3.Approx.LMN_active_moment {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (κ : ℝ) (n : ℕ) {k : ℤ} {t : ℝ} (hz : I.zetaMK m k t ≠ 0) : I.LMN κ m n t = I.hatZetaML m (lIdx β I.Λ m k) t * (4 * Real.pi ^ 2 * κ / epsilon β I.Λ m ^ 2) ^ n * cutoffMoment I κ m (lIdx β I.Λ m k) n t

theorem AVenhance.Infra.Section3.Approx.Jhat_active {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) {κ : ℝ} (hκ : 0 < κ) {k : ℤ} (hk : Odd k) {t : ℝ} (hz : I.zetaMK m k t ≠ 0) : I.Jhat κ m t = κ • 1 + (2 * Real.pi ^ 2 * a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 2 * I.zetaProd m k t * ∑ n ∈ Finset.range (Nstar β), (↑n.factorial)⁻¹ * iteratedDeriv n (I.zetaMK m k) t * cutoffMoment I κ m (lIdx β I.Λ m k) n t) • shearAxis k

theorem AVenhance.Infra.Section3.Approx.flux_sub_Jhat_active {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) {κ : ℝ} (hκ : 0 < κ) {k : ℤ} (hk : Odd k) {t : ℝ} (hz : I.zetaMK m k t ≠ 0) : I.flux κ m t - I.Jhat κ m t = (2 * Real.pi ^ 2 * a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 2 * I.zetaProd m k t * ∫ (s : ℝ) in Set.Iic t, I.hatZetaML m (lIdx β I.Λ m k) s * (I.zetaMK m k s - ∑ n ∈ Finset.range (Nstar β), (↑n.factorial)⁻¹ * (s - t) ^ n * iteratedDeriv n (I.zetaMK m k) t) * Real.exp (4 * Real.pi ^ 2 * κ / epsilon β I.Λ m ^ 2 * (s - t))) • shearAxis k

theorem AVenhance.Infra.Section3.Approx.shearAxis_entry_abs_le (k : ℤ) (i j : Fin 2) : |shearAxis k i j| ≤ 1

theorem AVenhance.Infra.Section3.Approx.Jhat_eq_kappa_of_no_odd_active {β : ℝ} (I : Ingredients β) (κ : ℝ) (m : ℕ) (t : ℝ) (hz : ∀ (k : ℤ), Odd k → I.zetaMK m k t = 0) : I.Jhat κ m t = κ • 1

theorem AVenhance.Infra.Section3.flux_sub_Jhat_entry_abs_le {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) {κ : ℝ} (hκ : 0 < κ) (t : ℝ) (i j : Fin 2) : |(I.flux κ m t - I.Jhat κ m t) i j| ≤ 4 * Real.pi ^ 2 * I.Czeta * ↑(Nstar β) * 2 ^ Nstar β * (a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 4 / κ) * (epsilon β I.Λ m ^ 2 / (κ * tau β I.Λ m)) ^ Nstar β

Entrywise e.JJhat for the actual flux and Jhat.

theorem AVenhance.Infra.Section3.flux_sub_Jhat_norm_le {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) {κ : ℝ} (hκ : 0 < κ) (t : ℝ) : ‖I.flux κ m t - I.Jhat κ m t‖ ≤ 4 * Real.pi ^ 2 * I.Czeta * ↑(Nstar β) * 2 ^ Nstar β * (a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 4 / κ) * (epsilon β I.Λ m ^ 2 / (κ * tau β I.Λ m)) ^ Nstar β

e.JJhat, in the elementwise supremum matrix norm, with an explicit constant depending only on the cutoff constant and the fixed Taylor budget.

theorem AVenhance.Infra.Section3.Approx.halfline_translate (t T : ℝ) (f : ℝ → ℝ) : ∫ (s : ℝ) in Set.Iic (t + T), f s = ∫ (s : ℝ) in Set.Iic t, f (s + T)

theorem AVenhance.Infra.Section3.LMN_periodic {β : ℝ} (I : Ingredients β) (κ : ℝ) (m n : ℕ) : Function.Periodic (I.LMN κ m n) (tauPP β I.Λ m)

The large memory coefficient has its actual large-cell period.

theorem AVenhance.Infra.Section3.Approx.periodic_iteratedDeriv {f : ℝ → ℝ} {P : ℝ} (hp : Function.Periodic f P) (r : ℕ) : Function.Periodic (iteratedDeriv r f) P

theorem AVenhance.Infra.Section3.Approx.LMN_unit_periodic {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (κ : ℝ) (n : ℕ) : Function.Periodic (I.LMN κ m n) 1

theorem AVenhance.Infra.Section3.Approx.qMNR_unit_periodic {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (κ : ℝ) (n r : ℕ) (i j : Fin 2) : Function.Periodic (fun (t : ℝ) => I.qMNR κ m n r t i j) 1

theorem AVenhance.Infra.Section3.Approx.periodic_primitive_pairing {f : ℝ → ℝ} {q : ℕ → ℝ → ℝ} (N : ℕ) (hf : ContDiff ℝ (↑↑N) f) (hp : Function.Periodic f 1) (hq : ∀ (r : ℕ), Continuous (q r)) (hqp : ∀ (r : ℕ), Function.Periodic (q r) 1) (hqd : ∀ (r : ℕ) (t : ℝ), HasDerivAt (q (r + 1)) (-q r t) t) : ∫ (t : ℝ) in 0..1, f t * q 0 t = ∫ (t : ℝ) in 0..1, iteratedDeriv N f t * q N t

theorem AVenhance.Infra.Section3.LMN_jMN_covariance_abs_le {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) {κ : ℝ} (hκ : 0 < κ) (hcondition : epsilon β I.Λ m ^ 2 ≤ κ * tau β I.Λ m / 2) {n : ℕ} (hn : n ≤ Nstar β) (i j : Fin 2) : |∫ (t : ℝ) in 0..1, I.LMN κ m n t * (I.jMN κ m n t i j - timeAvgMat (I.jMN κ m n) i j)| ≤ 2 * I.Czeta * ↑(Nstar β).factorial * 2 ^ Nstar β * 2 ^ Nstar β * I.Chat ^ 2 * 8 ^ Nstar β * (a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 4 / κ) * (tau β I.Λ m / tauP β I.Λ m) ^ Nstar β

Finite-regularity averaging of an actual jMN oscillation against LMN. The small factor is the ratio of the two cutoff time scales.

theorem AVenhance.Infra.Section3.Approx.Jhat_entry_continuous {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) {κ : ℝ} (hκ : 0 < κ) (i j : Fin 2) : Continuous fun (t : ℝ) => I.Jhat κ m t i j

theorem AVenhance.Infra.Section3.Approx.Kmat_entry_continuous {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) {κ : ℝ} (hκ : 0 < κ) (i j : Fin 2) : Continuous fun (t : ℝ) => I.Kmat κ m t i j

theorem AVenhance.Infra.Section3.Approx.timeAvgMat_sub_entry_eq_integral {F G : ℝ → Matrix (Fin 2) (Fin 2) ℝ} (i j : Fin 2) (hf : Continuous fun (t : ℝ) => F t i j) (hg : Continuous fun (t : ℝ) => G t i j) : (timeAvgMat F - timeAvgMat G) i j = ∫ (t : ℝ) in 0..1, (F t - G t) i j

theorem AVenhance.Infra.Section3.Jhat_average_sub_Khom_norm_le {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) {κ : ℝ} (hκ : 0 < κ) : ‖timeAvgMat (I.Jhat κ m) - I.Khom κ m‖ ≤ 4 * Real.pi ^ 2 * I.Czeta * ↑(Nstar β) * 2 ^ Nstar β * (a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 4 / κ) * (epsilon β I.Λ m ^ 2 / (κ * tau β I.Λ m)) ^ Nstar β

Averaging preserves the proved flux approximation error.

theorem AVenhance.Infra.Section3.Kmat_average_sub_Jhat_entry_abs_le {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) {κ : ℝ} (hκ : 0 < κ) (hcondition : epsilon β I.Λ m ^ 2 ≤ κ * tau β I.Λ m / 2) (i j : Fin 2) : |(timeAvgMat (I.Kmat κ m) - timeAvgMat (I.Jhat κ m)) i j| ≤ 2 * ↑(Nstar β) * I.Czeta * ↑(Nstar β).factorial * 2 ^ Nstar β * 2 ^ Nstar β * I.Chat ^ 2 * 8 ^ Nstar β * (a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 4 / κ) * (tau β I.Λ m / tauP β I.Λ m) ^ Nstar β

The oscillatory part of Jhat contributes a finite-regularity averaging error, with the actual time-scale ratio rather than an assumed analytic rate.

theorem AVenhance.Infra.Section3.Kmat_average_sub_Khom_norm_le_finite {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) {κ : ℝ} (hκ : 0 < κ) (hcondition : epsilon β I.Λ m ^ 2 ≤ κ * tau β I.Λ m / 2) : ‖timeAvgMat (I.Kmat κ m) - I.Khom κ m‖ ≤ a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 4 / κ * (4 * Real.pi ^ 2 * I.Czeta * ↑(Nstar β) * 2 ^ Nstar β * (epsilon β I.Λ m ^ 2 / (κ * tau β I.Λ m)) ^ Nstar β + 2 * ↑(Nstar β) * I.Czeta * ↑(Nstar β).factorial * 2 ^ Nstar β * 2 ^ Nstar β * I.Chat ^ 2 * 8 ^ Nstar β * (tau β I.Λ m / tauP β I.Λ m) ^ Nstar β)

A finite-regularity version of the average comparison, retaining both justified errors. No analytic averaging premise is silently added.