Port full corpus to Lean 4.31 + fix Option-cases default arm

[emeryberger]

Stacked on #5 (base = roundtrip-faithfulness) — merge that first.

The example corpus still used APIs removed/renamed in 4.31, so several modules failed to build and the full extraction (Corpus/CorpusTestCombined.lean) could not run. This ports every site to its 4.31 spelling and gets the whole corpus building + extracting cleanly again.

Corpus API ports

• List.bind -> List.flatMap (call sites only; the user-defined Option.bind/Either.bind/… defs are untouched)
• Array.swap! -> Array.swapIfInBounds
• Array.mkArray -> Array.replicate
• List.get? i -> xs[i]?
• List.enum -> List.zipIdx — the tuple order flips (i,v) -> (v,i), so the destructuring binders are swapped to preserve semantics
• String.drop now returns String.Slice -> .toString (Parsers)
• compare _ _ == .lt -> == Ordering.lt (the dotted-ident type is no longer inferable through ==)
• Matrix: def -> abbrev so m[i]? can synthesize GetElem? through the alias

Also adds Advanced and Production to the Corpus root so lake build covers the whole corpus, and regenerates extracted/lcnf_corpus.py from the ported sources (554 transpiled defs, valid Python).

One more transpiler bug

Extracting the full corpus surfaced a bug in emitOptionCases (LeanToPython.lean): it handled only the named Option.none/Option.some arms and dropped a default arm, producing an empty if:/else: block (IndentationError) for Option matches Lean compiled with a default — the same class of bug as the earlier emitListCases fix (PR #5). Now handles default on both branches with a pass safety net.

Verification

Whole corpus builds; full extraction is valid Python; Comprehensions/TailCalls/RegressionFixes suites, evaluate_correctness.py (0 wrong), and the round-trip harness (112/112 + 3807/3807) all pass.