Math and TheoryThree-uniform Berge-C₄ saturation: linear bounds with coefficients 5/8 and 3/4, the cone spectrum and exact small values
Problem and result
- Problem
- Three-uniform Berge-C₄ saturation number (English–Graber–Kirkpatrick–Methuku–Sullivan)
- Posed in
- English, Graber, Kirkpatrick, Methuku and Sullivan, Saturation of Berge hypergraphs, arXiv:1710.03735v1, Theorem 5.7 (upper bound n − 2)
- Status
- Linear coefficient bounded between 5/8 and 3/4; exact values for n ≤ 13
- Result
- For n ≥ 9, (5n − 3623)/8 ≤ sat₃(n, Berge-C₄) ≤ ⌈(3n − 9)/4⌉; saturated cones are classified and the values for n ≤ 13 are exact.
Abstract
The three-uniform Berge-C₄ saturation number s(n), in which any absent triple may be added, satisfies max(⌈(n − 1)/2⌉, ⌈(5n − 3623)/8⌉, ⌈(5n + 89)/8 − √(270n + 1891)/4⌉) ≤ s(n) ≤ ⌈(3n − 9)/4⌉ for every n ≥ 9, so 5/8 ≤ liminf s(n)/n ≤ limsup s(n)/n ≤ 3/4; the previous explicit upper bound was n − 2. The preprint classifies the saturated cones for n ≥ 5, whose sizes are exactly the integers from ⌈(3n − 5)/4⌉ to n − 2 together with n − 1 when n ≡ 1 (mod 3), proves that a vertex reached from every other vertex by paths of lengths one and two forces 3(n − 1)/4 hyperedges, and gives s(n) for n ≤ 13 from exhaustive certificates.
Details
- Year
- 2026
- Discipline
- Mathematics
- Area
- Extremal hypergraph theory
- Subject
- Graph theory and graph polynomials
- Result type
- Two-sided asymptotic bounds, structural classification and exact small values with reproducible proof package
- Formal proof
- Standalone Lean package
- Family
berge-c4-saturation- Keywords
- Berge hypergraphs, Berge cycles, Berge-C4, saturation numbers, three-uniform hypergraphs, saturation spectrum, extremal hypergraph theory
Statement and scope
Formal scope. Lean 4.35.0 proves, for actual three-uniform hypergraphs on Fin n, Berge-C₄s with distinct vertices and distinct hyperedges, and saturation under every absent triple, that for every n ≥ 9 a saturated hypergraph with ⌈(3n − 9)/4⌉ hyperedges exists, together with the general rooted-gluing theorem, the exact values for n ≤ 5 and the upper bounds for n = 6, 7, 8; explicit pieces are kernel-checked without native_decide. The lower bound, the cone classification and spectrum and the flexible-root theorem have conventional proofs, and the values for 6 ≤ n ≤ 13 rest on exhaustive certificates checked by an independent C++ verifier.
Lean 4.35.0 proves, for actual three-uniform hypergraphs, Berge-C₄s with distinct vertices and hyperedges, and saturation under every absent triple, that a saturated hypergraph with ⌈(3n − 9)/4⌉ hyperedges exists for every n ≥ 9, together with the exact values for n ≤ 5. The lower bound, the cone results and the flexible-root theorem are conventional; the values for 6 ≤ n ≤ 13 rest on certificates checked by an independent C++ verifier.
A Lean check establishes only the formal statement that is checked. It does not establish novelty, historical priority or a faithful transcription of an external source. Known gaps are listed in UNFINISHED.md; the authorship disclosure describes how the results were produced.
Manuscript
- PDF on this site
manuscript.pdf350 KB- PDF on GitHub
papers/mathematics/ berge-c4-saturation/ manuscript.pdf - LaTeX source
papers/mathematics/ berge-c4-saturation/ manuscript.tex
Formal proof
This result has a standalone Lean 4 package, separate from the shared library. Build it with the toolchain and instructions given in its README.
- Proof package
papers/mathematics/ berge-c4-saturation/ - Lean project
papers/6 Lean filesmathematics/ berge-c4-saturation/ lean/ - Lakefile
papers/mathematics/ berge-c4-saturation/ lean/ lakefile.toml - Toolchain
leanprover/lean4:v4.35.0 - Library roots
Reproduce
The commands below are quoted from papers/, which gives their context and working directory.
bash scripts/verify.sh /tmp/berge-c4-verificationFinite certificates
python3 certificate/run_certificates.py --json certificate-check.json- README
papers/mathematics/ berge-c4-saturation/ README.md - Verification guide
papers/mathematics/ berge-c4-saturation/ verification/ README.md - Verification record
papers/mathematics/ berge-c4-saturation/ VERIFICATION.md - Authorship
papers/mathematics/ berge-c4-saturation/ AUTHORSHIP.md - Repository guide
verification/README.md - Unfinished proofs
UNFINISHED.md
Source and prior work
Prior work. English, Graber, Kirkpatrick, Methuku and Sullivan, arXiv:1710.03735v1, Theorem 5.7. · English, Gerbner, Methuku and Tait, 2019.
Questions and answers
What is the three-uniform Berge-C4 saturation number?
It is the least number of hyperedges of a three-uniform hypergraph on n vertices with no Berge four-cycle in which adding any absent triple creates one. For n ≥ 9 it lies between max(⌈(n − 1)/2⌉, ⌈(5n − 3623)/8⌉, ⌈(5n + 89)/8 − √(270n + 1891)/4⌉) and ⌈(3n − 9)/4⌉, so its linear coefficient is between 5/8 and 3/4. Whether it equals ⌈(3n − 9)/4⌉ for all n ≥ 9 is open.
How does this compare with earlier bounds?
English, Graber, Kirkpatrick, Methuku and Sullivan gave the upper bound n − 2 for n ≥ 7, and connectivity gives the lower bound ⌈(n − 1)/2⌉; English, Gerbner, Methuku and Tait proved linear growth. The linear saturation problem studied by Wang and Zhang, where only additions preserving linearity are tested, is different. Searches in October 2026 did not find the coefficients 5/8 or 3/4; priority is not certified.
Is the result formally verified?
Partly. Lean 4 proves the upper construction for every n ≥ 9 and the exact values for n ≤ 5, with explicit pieces checked by the kernel. The lower bound, the cone classification and the flexible-root theorem have conventional proofs, and the values for 6 ≤ n ≤ 13 rest on exhaustive certificates checked by an independent verifier.
Cite
Citation file papers/. For the whole collection, use CITATION.cff or CITATION.bib.
@misc{goyal2026bergecfoursaturation,
author = {Goyal, Dev D.},
title = {Three-Uniform {Berge}-{$C_4$} Saturation: Linear Bounds with Coefficients 5/8 and 3/4, the Cone Spectrum and Exact Small Values},
year = {2026},
month = oct,
note = {Preprint. Fully autonomous agentic research; publication responsibility: Dev D. Goyal},
url = {https://github.com/dvgyl/math-and-theory/tree/main/papers/mathematics/berge-c4-saturation}
}