v1.2 — revised paper with the Lean formalisation (Appendices B–C)

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.

v1.1 — Lean formalisation of the ceiling theorems

Version of record. Paper unchanged from v1.0 (preprint of 8 September 2026).

New in v1.1: lean/ — a Lean 4 / Mathlib v4.23.0 formalisation of the two unconditional results, Theorem 3.1 (product ceiling, product_ceiling) and Theorem 3.4 (refined ceiling: hiding_bound, diagonal_bound, fixed_point_form, and refined_ceiling_numeric : c ≤ 0.3829), plus Lemma 3.3 for the i.i.d., all-couplings and mixtures-of-products classes. Zero sorry; axioms propext, Classical.choice, Quot.sound only; bash lean/check.sh is the gate and runs in CI on a fresh clone. lean/README.md maps every paper statement to its Lean name and lists what is not formalised (Proposition 2.2, the maximal-correlation class, everything conditional in Sections 5–6).

Assets: the paper (PDF), the LaTeX source with ancillary files, and verification-pack.zip (self-contained one-minute and four-hour re-runs of the numerical certificate, with CONFIRMED/FAILED reports).

v1.0 — preprint of 8 September 2026

Version of record of the preprint The ceiling of the single-letter entropy method for the union-closed sets conjecture, and a protocol that reaches it (Andrew Moffat, 8 September 2026).

Assets: the paper (PDF) and the LaTeX source with ancillary files. The repository at this tag contains the code, every log, four referee reports, the independent re-certification and a one-minute verification script (python verify.py --search).

Results: two unconditional ceiling theorems for the single-letter entropy method (c_ceil = 0.383099…, c** = 0.382885260…), and a computer-assisted, conditional lower bound c_0 ≥ 0.38284 for the union-closed constant (previous record 0.382709, Liu 2023). Frankl's conjecture itself remains open.