theorem G12LocalScale.endpoint_coordinate {N r : ℝ} (hN : 1 < N) (hlo : N ^ (4 / 53) ≤ r) (hhi : r ≤ N ^ (1 / 10)) : 4 / 53 ≤ Real.log r / Real.log N ∧ Real.log r / Real.log N ≤ 1 / 10

The actual prime endpoint retains its original lower and upper coordinates.

theorem G12LocalScale.source_domain_nonempty {N e : ℝ} (hN : 1 ≤ N) (he : e ≤ 1) : ∃ (x : ℝ) (T : ℝ) (r : ℝ), e * N ≤ x ∧ x ≤ 4 * N ∧ N ^ (4 / 53) / 2 ≤ T ∧ T ≤ r ∧ N ^ (4 / 53) ≤ r ∧ r ≤ N ^ (1 / 10)

A concrete witness rules out empty-domain admission for every source epsilon.

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

One source-faithful cutoff controls admission, internal level and the main coefficient simultaneously. In particular x may be the physical value 4*M*T; no equality between the local and ambient scales is assumed.