theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.g9Scale_level_identity (x T ν ε : ℝ) (hx : 0 < x) (hT : T = x ^ ν) : x ^ ((5 - 5 * ν) / 9 - ε) = x ^ (5 / 9 - ε) / T ^ (5 / 9)

Numerical level conversion, not a transport theorem for well-factorability.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.g9Scale_eventually_level_numerator (K ε δ : ℝ) (hK : 1 ≤ K) (hε : ε ≤ 5 / 9) (hδε : ε < δ) : ∀ᶠ (N : ℝ) in Filter.atTop, ∀ (x : ℝ), N / K ≤ x → N ^ (5 / 9 - δ) ≤ x ^ (5 / 9 - ε)

The positive gap δ - ε absorbs the fixed scale distortion K^(5/9-ε). The threshold is independent of the local scale x.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.g9Scale_eventually_local_global_and_level (K ε α δ : ℝ) (hK : 1 ≤ K) (hε : 0 < ε) (hεα : ε < α) (hα : α ≤ 1 / 10) (hδε : ε < δ) : ∀ᶠ (N : ℝ) in Filter.atTop, ∀ (x T : ℝ), N / K ≤ x → x ≤ 4 * N → N ^ α / 2 ≤ T → T ≤ N ^ (1 / 10) → have ν := Real.log T / Real.log x; 1 < x ∧ 1 ≤ T ∧ T = x ^ ν ∧ ε ≤ ν ∧ ν ≤ 1 / 10 + ε / 10 ∧ N ≤ K * x ∧ N ^ (5 / 9 - δ) / T ^ (5 / 9) ≤ x ^ ((5 - 5 * ν) / 9 - ε)

Full uniform scale bridge with the optional genuine numerical level comparison. Only fixed parameter restrictions and the original rectangle bounds are inputs.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.g9Scale_exists_threshold_local_global_and_level (K ε α δ : ℝ) (hK : 1 ≤ K) (hε : 0 < ε) (hεα : ε < α) (hα : α ≤ 1 / 10) (hδε : ε < δ) : ∃ (N₀ : ℝ), ∀ (N : ℝ), N₀ ≤ N → ∀ (x T : ℝ), N / K ≤ x → x ≤ 4 * N → N ^ α / 2 ≤ T → T ≤ N ^ (1 / 10) → have ν := Real.log T / Real.log x; 1 < x ∧ 1 ≤ T ∧ T = x ^ ν ∧ ε ≤ ν ∧ ν ≤ 1 / 10 + ε / 10 ∧ N ≤ K * x ∧ N ^ (5 / 9 - δ) / T ^ (5 / 9) ≤ x ^ ((5 - 5 * ν) / 9 - ε)

Explicit quantifier-order interface: one cutoff works for every local block.