Version of record.
Paper (31 pp): the 8 September preprint plus Appendix B (the finite model, the Lean statements verbatim with file/line references, what is not formalised, the certificate) and Appendix C (the complete Lean source, byte-identical to lean/). Sections 2–7 and Appendix A are unchanged; theorem numbering is unchanged. Compiles with XeLaTeX (Tectonic).
Formal verification: Theorems 3.1 and 3.4 (product_ceiling; hiding_bound, diagonal_bound, fixed_point_form, refined_ceiling_numeric : c ≤ 0.3829) and Lemma 3.3 for the i.i.d., all-couplings and mixtures-of-products classes, in Lean 4.23.0 / Mathlib v4.23.0. Zero sorry; axioms propext, Classical.choice, Quot.sound only. Gate bash lean/check.sh passes locally and in CI on a fresh Ubuntu clone. LEAN-CERTIFICATE.md records the commit, toolchain, #print axioms output and SHA-256 of every source and build file. An independent referee pass (28 findings, all applied) checked every quoted statement and listing against the sources.
Assets: paper.pdf; union-closed-arxiv.tar.gz (paper.tex + anc/ including anc/lean/); verification-pack.zip (self-contained one-minute and four-hour re-runs of the numerical certificate); LEAN-CERTIFICATE.md.