Unlike \(\eta\) (three dedicated Lean files) or the criticality bridge (Theorem C.1, derived fully in 102), \(\rho\) does not currently have a dedicated Lean formalization file in AXLE analogous to TribonacciRatioConvergence.lean. The exact formula \(\rho(P_M)=1/2^{{M-1}}\) is elementary enough that a Lean proof would be a short, mechanical induction (similar in spirit to 102’s orbit_halving attempt) — genuinely tractable, currently unwritten. The numerical estimate \(\rho(\mathcal{{L}})\approx0.751\), by contrast, depends on a weighted-drift computation over the transfer operator that would need real numerical-analysis infrastructure (rigorous interval bounds on an infinite sum, similar in spirit to Week 4’s bracketing argument for \(\Sigma\), but over a function space rather than a single polynomial) to formalize with any confidence.
rho_PM_eq (M : ℕ) : ρ(P_M) = 1 / 2^(M-1) as an actual Lean lemma is tractable at this course’s level, following the exact pattern 102 Week 12 established: state it, attempt the proof, and if it closes cleanly, it’s a real candidate contribution to AXLE. The \(\rho(\mathcal{{L}})\) numerical bound is a genuinely harder, longer-term project — correctly scoped as beyond this course, not glossed over as easy.
-- dm³ 103 · Week 11 · ρ formalization audit — honest gap -- NOT YET in AXLE (unlike η's 3 files): -- rho_PM_eq (M) : ρ(P_M) = 1 / 2^(M-1) -- tractable, unwritten -- rho_L_bound : |ρ(ℒ) - 0.751| < ε -- genuinely harder -- (needs rigorous interval bounds on infinite sum) -- Exercise: attempt rho_PM_eq as a short induction on M, following -- the orbit_halving pattern from 102 Week 12. example : True := trivial