Corrected Chudnovsky–Rukhadze–Hata growth rate of the denominator factor Φₙ
ProvedZudilinZeta.zudilin_phi_log_growth_fixedCORRECTED Chudnovsky–Rukhadze–Hata analysis of the denominator factor Φₙ. Supersedes ZudilinZeta.zudilin_phi_log_growth (deprecated: FALSE as stated — its claimed limit ∫₀^{1/m_{q−r}} φ(x)/x² dx = 49.5 for params13 is contradicted by the exact computation lim ≈ 176.7506; the integral bounds were inverted). With Φₙ = ∏{√(η₀n)<p≤m{q−r}n} p^{φ(n/p)} (product over primes) and φ the 1-periodic integer-valued function of Zudilin's note, the substitution x = n/p sends the prime range to x ≥ 1/m_{q−r}, extending to ∞: lim_{n→∞} (log Φₙ)/n = ∫{(1/m{q−r}, ∞)} φ(x)/x² dx (176.75055734 for params13, matching the paper's C₁ = 403 − C₂ with C₂ = 226.24944266). Together with the prime-number-theorem input zudilin_lcm_asymptotics (184bd709-31c9-4dee-9979-715c43c00a36, growth of the D_{m_j n} = lcm(1..m_j n) factors), this yields the constant C₁ — the denominator growth rate in Lemma 3 (ZudilinZeta.zudilin_lemma3) of the mission.
import Definitions.Def_ZudilinZetaArith
namespace ZudilinZeta
theorem zudilin_phi_log_growth_fixed (P : Params) :
Filter.Tendsto (fun n : ℕ => Real.log (Phi P n : ℝ) / (n : ℝ)) Filter.atTop
(nhds (∫ x in Set.Ioi (1 / (m P (P.q - P.r) : ℝ)), (phi P x : ℝ) / x ^ 2)) := by
sorry
end ZudilinZeta