Uniform comparison of the κ chain with κ′. The high scales use the summable averaging loss; only the finitely many lower scales use the coarse flux cap.

theorem AVenhance.Infra.Section3.KappaAtPrimeScaleComparison.kappaAtPrime_ratio_high {β C₀ : ℝ} (I : Ingredients β) (hCz : I.Czeta ≤ C₀) (hCh : I.Chat ≤ C₀) {κ : ℝ} (hκ : 0 < κ) {M N : ℕ} (hpermitted : κ ∈ permittedInterval β I.Λ M) (hN : 1 ≤ N) (hTail : kappaAtBootstrapTail β (kappaAtBootstrapErrorCoefficient β C₀ 2) N ≤ 1 / 2) (m d : ℕ) : m + d = M → N ≤ m → max (I.kappaAt κ m d / kappaPrimeAt β I.Λ κ m d) (kappaPrimeAt β I.Λ κ m d / I.kappaAt κ m d) ≤ (1 - kappaAtBootstrapTail β (kappaAtBootstrapErrorCoefficient β C₀ 2) m)⁻¹

theorem AVenhance.Infra.Section3.KappaAtPrimeScaleComparison.kappaAtPrime_ratio_low_segment {β C₀ : ℝ} (I : Ingredients β) (hCz : I.Czeta ≤ C₀) (hCh : I.Chat ≤ C₀) {κ : ℝ} (hκ : 0 < κ) {M base : ℕ} (hpermitted : κ ∈ permittedInterval β I.Λ M) (hbaseM : base ≤ M) (hbaseRatio : max (I.kappaAt κ base (M - base) / kappaPrimeAt β I.Λ κ base (M - base)) (kappaPrimeAt β I.Λ κ base (M - base) / I.kappaAt κ base (M - base)) ≤ 2) (m k : ℕ) : m + k = base → 1 ≤ m → max (I.kappaAt κ m (M - m) / kappaPrimeAt β I.Λ κ m (M - m)) (kappaPrimeAt β I.Λ κ m (M - m) / I.kappaAt κ m (M - m)) ≤ kappaAtBootstrapIteratedBound β C₀ k

theorem AVenhance.Infra.Section3.kappaAt_kappaPrime_uniform_ratio_bound {β C₀ : ℝ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hC₀ : 0 ≤ C₀) : ∃ (R : ℝ), 1 ≤ R ∧ ∀ (I : Ingredients β), I.Czeta ≤ C₀ → I.Chat ≤ C₀ → ∀ (κ : ℝ), 0 < κ → ∀ (M : ℕ), 1 ≤ M → κ ∈ permittedInterval β I.Λ M → ∀ (m : ℕ), 1 ≤ m → m ≤ M → max (I.kappaAt κ m (M - m) / kappaPrimeAt β I.Λ κ m (M - m)) (kappaPrimeAt β I.Λ κ m (M - m) / I.kappaAt κ m (M - m)) ≤ R

An unconditional factor comparing the and auxiliary κ chains on all scales 1 ≤ m ≤ M. The cutoff and the finite low-scale product depend only on β and C₀.