theorem G12LocalScale.coefficient_of_logs {N x T r ζ δ : ℝ} (hN : 1 < N) (hx : 1 < x) (hT : 0 < T) (hTr : T ≤ r) (hr : r ≤ N ^ (1 / 10)) (hz : 0 < ζ) (hzsmall : ζ ≤ 1 / 100) (hsmall : 48 * ζ ≤ δ) (hxl : (1 - ζ / 4) * Real.log N ≤ Real.log x) (hQl : Real.log N / 3 ≤ Real.log (level x T ζ)) : 4 * Real.log N / Real.log (level x T ζ) ≤ 36 / (5 * (1 - Real.log r / Real.log N)) + δ

The endpoint can vary independently after the local scale is admitted.

theorem G12LocalScale.uniform_coefficient (δ : ℝ) (hδ : 0 < δ) : ∃ (ζ : ℝ), 0 < ζ ∧ ζ ≤ 1 / 100 ∧ ∀ (e : ℝ), 0 < e → ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → ∀ (x T r : ℝ), e * ↑N ≤ x → x ≤ 4 * ↑N → ↑N ^ (4 / 53) / 2 ≤ T → T ≤ r → r ≤ ↑N ^ (1 / 10) → 4 * Real.log ↑N / Real.log (level x T ζ) ≤ 36 / (5 * (1 - Real.log r / Real.log ↑N)) + δ

Any requested coefficient slack is fixed before all scales and endpoints.