catalan-sun-lean v0.1.0 First software release: Lean 4 / Mathlib formalization of high-ROI structural lemmas from Zhi-Wei Sun, Catalan's constant is irrational (arXiv:2609.04176v1). Proved in this release Theorem 2.1 and Corollary 2.1 (absolute) Det-level Lemma 5.4 Pascal–Cauchy / Newton / Structure / Qhat stack through (4.5) Theorem 5.1 — unconditional (thm_5_1) Lemma 5.5 in full — row-stability (5.2) and ledger little-o (5.3) Corollary 5.2 §5 content — positive-part collapse and model comparison to o(B²) (Cor52.lean) Toolchain: Lean 4.32.2 / Mathlib v4.32.2. Verify: lake build (see results/lean_verify_brief.md: 0 sorry, axioms ⊆ classical three). Accompanying numerical note (in-repo) PAPER1_DRAFT_v4.pdf and scripts/gates/ document an independent measurement of the paper's §9 scalar inequality at B = 200…1000 (reported failure of the claimed B² sign). That note is not a claim that Theorem 1.1 is settled either way, and it is separate from Sun's arXiv paper. Not claimed Theorem 1.1 (Catalan's constant irrational) Props 6.3 / 7.4, Mertens / PNT, or a complete §4→§5 odd-p valuation bridge to H_B^min / q̂_B Cite Prefer the Zenodo software concept DOI once minted (GitHub→Zenodo webhook is enabled). Keep this software record separate from any future paper DOI for PAPER1 / Sun's preprint.