The file’s own \(\S\)7 names the two open gaps precisely. Sorry #A (orbit unrolling, \(n\equiv1\bmod4\) branch): needs lemma orbit_halving (m k : ℕ) (hdvd : 2^k ∣ m) : orbit m k = m / 2^k — an elementary induction on \(k\), described in the file as “fully provable in Lean with existing Mathlib,” omitted only because wiring it into the surrounding proof needs roughly 15 more lines of bookkeeping.
Sorry #B (\(n\equiv3\bmod4\) branch): genuinely harder. Strong induction on \(n\)’s value fails here, because one odd step from \(n\equiv3\bmod4\) produces \((3n+1)/2>n\) — the induction hypothesis doesn’t apply to a larger number. The file’s documented fix: induct on \(\text{{Nat.log}}_2 n\) (bit-length) instead of on \(n\) directly. A “double burst” (one odd step, then repeated bursts) multiplies by less than \((3/2)^2=9/4<4\), so the bit-length grows by at most 1 per double-step, and the number of times the orbit can stay above \(n\) is bounded — this is the standard Terras/Everett argument for Collatz, made constructive.
-- dm³ 102 · Week 11 · The two open gaps, precisely -- Sorry #A (n ≡ 1 mod 4): needs -- lemma orbit_halving (m k) (hdvd : 2^k ∣ m) : orbit m k = m / 2^k -- "Fully provable with existing Mathlib" — elementary induction on k, -- omitted only for ~15 lines of wiring/bookkeeping. -- Sorry #B (n ≡ 3 mod 4): genuinely harder. -- Strong induction on VALUE fails: one odd step gives (3n+1)/2 > n. -- Fix: induct on Nat.log 2 n (bit-length) instead — the standard -- Terras/Everett argument, made constructive. "Double burst" -- multiplies by < 9/4 < 4, bounding bit-length growth. -- File's own correction: "~80-100 lines... NOT ~40 lines... the -- earlier claim... was incorrect... Both sorries are mathematically -- closeable; neither is trivial." — an honest re-scoping, in the -- actual source, not a hypothetical example. example : True := trivial