Milestone task: attempt rho_PM_eq (M : ℕ) (hM : 1 ≤ M) : rho_PM M = 1 / 2^(M-1), where rho_PM is defined via the fixed-point eigenvalue argument from Week 9 (\(n=1\) fixed mod \(2^M\) for all \(M\), each row of \(P_M\) scaled by \(1/2^{{M-1}}\)). This is a genuine, if modest, formalization task: define the matrix structure precisely enough that the eigenvalue claim is a real theorem statement, not just an assertion.
FibonacciRatioConvergence.lean. 102 asked you to attempt orbit_halving. This is the same kind of task, scoped appropriately for where the course has arrived: find the real, currently-missing lemma, attempt it honestly, and submit it as a candidate PR against github.com/TOTOGT/AXLE whether or not it closes cleanly on the first attempt. If you get stuck, document precisely where and why — that’s itself useful, following the §7-style honest accounting CollatzDescent.lean modeled in 102.
-- dm³ 103 · Week 12 · Milestone VII — ρ(P_M) attempt
-- Define P_M precisely enough to state and attempt:
lemma rho_PM_eq (M : ℕ) (hM : 1 ≤ M) :
True := by -- replace with real matrix/eigenvalue statement
sorry -- your attempt goes here
-- Submit whether or not it closes. If stuck, document precisely
-- where, following CollatzDescent.lean §7's honest-accounting model.
example : True := trivial