Skip to content

v1.1 — Lean formalisation of the ceiling theorems

Choose a tag to compare

View all tags
@moffatstudio moffatstudio released this 10 Sep 19:46
· 2 commits to master since this release
v1.1
45949fa

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).

Assets 5
Loading