What is not proved: the general odd case for \(n\ge9\) has two explicit CollatzDescent.lean formalizes the Collatz step function directly: step n = if n even then n/2 else 3*n+1, orbit n k = step^[k] n (k-fold iteration), and works toward theorem descent (n : ℕ) (hn : 2 ≤ n) : ∃ k, orbit n k < n — every orbit eventually dips below its starting value. This is proved by strong induction, dispatching on parity: the even case is a one-line consequence of \(n/2v2 (2-adic valuation) and its behavior under even/odd splitting, two_pow_v2_dvd, the “burst” lemmas for \(n\equiv1\) and \(n\equiv3\pmod4\) (v2_mod4_one, burst_lt_mod4_one, v2_mod4_three, burst_exceeds_mod4_three), the even-descent case, and the small odd cases \(n\in\{{3,5,7\}}\) — these last three closed by native_decide, literally running the computation inside Lean’s kernel and checking the result.
sorrys, and the file documents both honestly in its own §7, “Honest Accounting of the Two Remaining Admits” — worth reading verbatim rather than summarizing, since it’s a genuinely good model of how to scope an open proof precisely. Week 11 covers exactly what those two gaps are and what closing them would take.
-- dm³ 102 · Week 10 · CollatzDescent.lean — real, honestly scoped
def step (n : ℕ) : ℕ := if n % 2 = 0 then n / 2 else 3 * n + 1
def orbit (n k : ℕ) : ℕ := step^[k] n
-- FULLY PROVED (0 sorry):
-- v2, two_pow_v2_dvd, v2_mod4_one, burst_lt_mod4_one,
-- v2_mod4_three, burst_exceeds_mod4_three
-- descent_even (n even ⟹ orbit n 1 < n)
-- descent for n ∈ {3,5,7} (via native_decide, kernel computation)
-- theorem descent (n) (hn : 2 ≤ n) : ∃ k, orbit n k < n
-- Even case + n∈{3,5,7}: proved.
-- General odd case (n≥9): 2 sorries — see Week 11.
example : True := trivial