theorem G12LocalScale.eventually_offset (c ζ : ℝ) (hz : 0 < ζ) : ∀ᶠ (N : ℕ) in Filter.atTop, c ≤ ζ / 4 * Real.log ↑N

All fixed logarithmic offsets are absorbed before introducing local cells.

theorem G12LocalScale.endpoint_logs {N e x T ζ : ℝ} (hN : 1 < N) (he : 0 < e) (heoff : |Real.log e| ≤ ζ / 4 * Real.log N) (h4off : Real.log 4 ≤ ζ / 4 * Real.log N) (h2off : Real.log 2 ≤ ζ / 4 * Real.log N) (hxlo : e * N ≤ x) (hxhi : x ≤ 4 * N) (hTlo : N ^ (4 / 53) / 2 ≤ T) (hThi : T ≤ N ^ (1 / 10)) : 0 < x ∧ 0 < T ∧ (1 - ζ / 4) * Real.log N ≤ Real.log x ∧ Real.log x ≤ (1 + ζ / 4) * Real.log N ∧ (4 / 53 - ζ / 4) * Real.log N ≤ Real.log T ∧ Real.log T ≤ 1 / 10 * Real.log N

Source endpoints give uniform logarithmic coordinates without setting x=N.

theorem G12LocalScale.uniform_admission (e ζ η : ℝ) (he : 0 < e) (hz : 0 < ζ) (hzsmall : ζ ≤ 1 / 100) (hη : 0 < η) (hηsmall : η < 1 / 8) : ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → ∀ (x T : ℝ), e * ↑N ≤ x → x ≤ 4 * ↑N → ↑N ^ (4 / 53) / 2 ≤ T → T ≤ ↑N ^ (1 / 10) → 1 < x ∧ 0 < T ∧ x ^ nu x T = T ∧ ζ ≤ nu x T ∧ nu x T ≤ 1 / 10 + ζ / 10 ∧ ↑N ^ (1 / 3) ≤ level x T ζ ∧ level x T ζ ≤ ↑N ∧ 2 ≤ MathlibNt.SieveTheory.LiLiuPrereqWF.externalInternalLevel (level x T ζ) η

Uniform local admission, with one cutoff before x,T and every later cell.