Math and TheoryThe upper saturation spectrum of Berge triangles in triple systems
Problem and result
- Problem
- Saturation spectrum of the Berge triangle in triple systems (Bushaw–English–Heath–Johnston–Rombach)
- Posed in
- Bushaw, English, Heath, Johnston and Rombach, The saturation spectrum of Berge stars, arXiv:2502.17686 (2025), Section 6
- Status
- Partially resolved
- Result
- For n ≥ 8 every saturated Berge-triangle-free triple system with more than ⌊(n−1)²/8⌋ edges is a paired product F(n,p), so the spectrum above this sharp threshold is exactly {p(n−2p)}.
Abstract
For every n ≥ 8, a Berge-triangle-free triple system on n vertices with more than ⌊(n−1)²/8⌋ edges lies inside a paired product F(n,p): p disjoint pairs, the other n − 2p vertices, and all triples formed by one pair and one other vertex. Saturated systems above this threshold are therefore paired products, and the saturation spectrum there consists exactly of the sizes p(n − 2p) up to Győri's maximum ⌊n²/8⌋. The threshold is sharp, since a saturated system with exactly ⌊(n−1)²/8⌋ edges that is not a paired product exists for every n ≥ 8. About n/4 sizes lie in the window and n/4 − O(√n) of them are missing, so the missing sizes near the top are not finitely many uniformly in n.
Details
- Year
- 2026
- Discipline
- Mathematics
- Area
- Graph theory
- Subject
- Graph theory and graph polynomials
- Result type
- Sharp structural threshold and reproducible proof package
- Formal proof
- Standalone Lean package
- Family
berge-triangle-spectrum- Keywords
- Berge triangle, saturation spectrum, triple systems, 3-uniform hypergraphs, Berge-triangle-free, paired product, stability, extremal hypergraph theory
Statement and scope
Formal scope. Lean 4.35.0 proves that paired products are Berge-triangle-free and saturated with p(n−2p) edges, that for every n ≥ 8 the explicit system J(⌊n/4⌋, n−2⌊n/4⌋) is saturated, is not a paired product and has exactly ⌊(n−1)²/8⌋ edges, and the arithmetic of the window, including the explicit deficits and at least ⌊n/4⌋ − ⌊√(2n)⌋/2 − 1 sizes there that are not of the form p(n−2p). It derives the upper spectrum and the maximum ⌊(n−1)²/8⌋ for saturated nonproducts from the containment theorem, which enters as a hypothesis and has a conventional proof, checked computationally for small orders.
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.pdf289 KB- PDF on GitHub
papers/mathematics/ berge-triangle-spectrum/ manuscript.pdf - LaTeX source
papers/mathematics/ berge-triangle-spectrum/ 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-triangle-spectrum/ - Lean project
papers/7 Lean filesmathematics/ berge-triangle-spectrum/ lean/ - Lakefile
papers/mathematics/ berge-triangle-spectrum/ 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.
python3 verify.py --output /tmp/berge-triangle-verification- README
papers/mathematics/ berge-triangle-spectrum/ README.md - Verification guide
papers/mathematics/ berge-triangle-spectrum/ verification/ README.md - Verification record
papers/mathematics/ berge-triangle-spectrum/ VERIFICATION.md - Authorship
papers/mathematics/ berge-triangle-spectrum/ AUTHORSHIP.md - Repository guide
verification/README.md - Unfinished proofs
UNFINISHED.md
Source and prior work
Prior work. Bushaw, English, Heath, Johnston and Rombach, 2025. · Frankl, Füredi, Goorevitch, Holzman and Simonyi, 2026.
Questions and answers
What is the saturation spectrum of the Berge triangle near the maximum?
For n ≥ 8, a Berge-triangle-saturated triple system on n vertices with more than ⌊(n−1)²/8⌋ edges is a paired product F(n,p), so the sizes above this threshold that occur are exactly the numbers p(n−2p) up to Győri's maximum ⌊n²/8⌋. For 0 ≤ d < ⌊n²/8⌋ − ⌊(n−1)²/8⌋, the size ⌊n²/8⌋ − d occurs exactly when d = 2j² (n ≡ 0 mod 4), d = 2j(j+1) (n ≡ 2 mod 4) or d = j(j+1)/2 (n odd). The spectrum at or below the threshold is not determined.
Are only finitely many sizes near the top missing?
No, not uniformly in n. The window above ⌊(n−1)²/8⌋ has about n/4 integers, of which n/4 − O(√n) are missing; for n = 400 only 8 of the 100 sizes above 19900 occur. This addresses the uniform reading of a suspicion of Bushaw, English, Heath, Johnston and Rombach, which was not stated as a numbered conjecture.
Is the threshold sharp, and what is formally verified?
Yes. For every n ≥ 8 an explicit saturated system with exactly ⌊(n−1)²/8⌋ edges is not a paired product. Lean 4 proves this construction for every n ≥ 8, that every paired product is Berge-triangle-free and saturated with the stated number of edges, and the arithmetic of the window. The containment theorem has a conventional proof and exact computer checks for small orders; Lean derives the spectrum statements and the sharp maximum from it as a hypothesis. Historical priority is not certified.
Cite
Citation file papers/. For the whole collection, use CITATION.cff or CITATION.bib.
@misc{goyal2026bergetrianglespectrum,
author = {Goyal, Dev D.},
title = {The Upper Saturation Spectrum of {Berge} Triangles in Triple Systems},
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-triangle-spectrum}
}