A Lean-verified proof of the empty-set-free height-five case of Frankl's conjecture
Abstract
Unrefereed AI-assisted preprint, version 0.4.1, 9 October 2026. Every finite nonempty union-closed family of distinct nonempty finite sets with inclusion height at most five has an element occurring in strictly more than half its members. Height counts members in a strict inclusion chain. This is the empty-set-free height-five theorem, not unrestricted Frankl's conjecture or the arbitrary empty-set-free height-six case. The complete encoded main theorem in HeightFive.lean is verified in Lean 4.34.1 using mathlib commit d13f23b723b8a846827a245b89c10fc7d3f11612. Its public assumptions are union closure, a nonempty family, absence of the empty member, and height at most five; coatom, critical-coordinate, projection-count and minimality conditions are derived, not additional assumptions. The 15 source modules and native rebuild logs are included. The final theorem reports only propext, Classical.choice and Quot.sound, with no sorryAx or theorem-specific added axiom. Formal verification certifies this encoded statement, not novelty, priority or human peer review. The stronger three-critical-coordinate preparatory lemma is not separately formalized; the main theorem requires only two. The current passing logs record a fresh 9 October 2026, 20:09-20:25 JST native rebuild of all 15 sources. The earlier successful version-0.4.0 logs are retained as history. All 15 sources match that earlier development byte for byte, and the frozen baseline payload hashes were independently checked again for this editorial release. Preparatory arguments and projection counts are attributed to Tian, arXiv:2608.25147v1. The manuscript identifies the additional universal-coatom selection, relative-coatom and majority-trimming steps, distinguishes the nearby Colbert, Bouchard and Zeng restricted results, and does not claim a separate proof of Tian's Problem 6.4 transfer inequalities. Global novelty and priority are not certified. 本研究は、清水竣平が個人の自主研究として企画・進行した、AIを活用した数学探索です。清水は探索方針の指示、検証の手配、成果の取りまとめを担当しました。証明の構成、計算による検証、原稿作成の大部分にはAIを使用しています。検証方法とその範囲は本文に記載しており、人間の専門家による査読は未実施です。 This work is an AI-assisted mathematical exploration initiated and coordinated by Shunpei Shimizu as a personal independent research project. Shimizu directed the exploration, arranged verification, and compiled the results. AI systems performed most proof construction, computational checking, and manuscript preparation. The verification methods and their scope are documented in the manuscript. The work has not received specialist human peer review. AI also performed most formalization; the submitter has not independently certified every mathematical step. No endorsement by cited researchers or institutions is implied. Read FRANKL_HEIGHT_FIVE_PREPRINT_v0.4.1.md first. The clean source package is Frankl_height5_publication_v0.4.1_20261009.zip; FRANKL_README_PUBLICATION_v0.4.1_EN_r1.md explains verification and contents. Version 0.4.1 integrates contribution and attribution corrections; the main theorem, Sections 2 through 7.2, all displayed identities and all Lean sources are unchanged from version 0.4.0. Earlier manuscripts, private-review addenda, staging READMEs and partial-verification records are retained as dated history, not the current preprint. Their earlier scope and private-draft statements do not override this current version. No PDF has been generated for the Markdown manuscript.
