Milestone task: attempt orbit_halving (m k : ℕ) (hdvd : 2^k ∣ m) : orbit m k = m / 2^k, the tractable gap from Week 11. Base case: \(k=0\), \(\text{{orbit}}\,m\,0=m=m/1\), trivial by definition. Inductive step: assuming \(\text{{orbit}}\,m\,k=m/2^k\) for \(2^k\mid m\), show \(\text{{orbit}}\,m\,(k{{+}}1)=\text{{step}}(\text{{orbit}}\,m\,k)=\text{{step}}(m/2^k)\); since \(2^{{k+1}}\mid m\), the quotient \(m/2^k\) is even, so \(\text{{step}}(m/2^k)=(m/2^k)/2=m/2^{{k+1}}\), closing the induction.
CollatzDescent.lean file is missing, needed to close its \(n\equiv1\bmod4\) branch. If your proof compiles cleanly, it is a legitimate candidate for a pull request against github.com/TOTOGT/AXLE, following the same pattern 101 established for FibonacciRatioConvergence.lean: find the real gap, close it for real, submit it. Sorry #B (the \(n\equiv3\bmod4\) branch, Week 11) is the harder milestone for anyone who wants to go further — described honestly in the source as genuinely non-trivial, not a quick follow-up.
Submission: your orbit_halving proof (compiling or not — document where it breaks if it doesn’t close cleanly), plus a short note on whether you see a path to Sorry #B using the Nat.log 2 strategy from Week 11. Phase III is closed — Week 13 opens the synthesis phase with \(G^5\).
-- dm³ 102 · Week 12 · Milestone IV — orbit_halving attempt
lemma orbit_halving (m k : ℕ) (hdvd : 2 ^ k ∣ m) :
orbit m k = m / 2 ^ k := by
induction k with
| zero => simp [orbit]
| succ k ih =>
-- 2^(k+1) ∣ m ⟹ 2^k ∣ m, apply ih, then one more halving step
sorry -- your attempt goes here
-- If this closes with 0 sorry, it's a real candidate PR against
-- github.com/TOTOGT/AXLE — the actual gap CollatzDescent.lean names.
example : True := trivial