Math and TheoryExact Berge saturation numbers of the subdivided star in every uniformity and its minimality among trees
Problem and result
- Problem
- Berge saturation numbers of trees and the Berge analogue of the minimum-tree theorem of Faudree, Faudree, Gould and Jacobson
- Posed in
- English, Graber, Kirkpatrick, Methuku and Sullivan, Saturation of Berge hypergraphs, arXiv:1710.03735; graph case: Faudree, Faudree, Gould and Jacobson, Saturation numbers for trees, Electron. J. Combin. 16 (2009), R91
- Status
- Exact formula proved in every uniformity; minimality among trees proved for three-uniform hypergraphs
- Result
- sat_r(n, Berge-B_a) = ⌊a(n + 1)/((r − 1)a + 1)⌋ for a, r ≥ 3 and n ≥ (r − 1)a + 1; for a ≥ 5, B_a is the unique tree on a + 2 vertices with the least three-uniform saturation coefficient.
Abstract
Let B_a be the star K_{1,a} with one edge subdivided. For all a, r ≥ 3 and n ≥ (r − 1)a + 1 the r-uniform Berge saturation number, in which any absent r-set may be added, is sat_r(n, Berge-B_a) = ⌊a(n + 1)/((r − 1)a + 1)⌋, attained by disjoint loose stars; it is a for max(a + 2, r + 1) ≤ n < (r − 1)a + 1. Saturated hypergraphs within k hyperedges of the minimum consist of loose stars with at least a spokes and at most (r − 1)((r − 1)a + 1)(k + 1) − 1 further vertices once n ≥ ((r − 1)a + 1)((r − 1)(k + 1) + 1), sharply for k = 0. For a ≥ 5 every tree T ≇ B_a on a + 2 vertices has sat₃(n, Berge-T) ≥ ⌈(a + 1)(n − 2)/(2a + 3)⌉, so B_a is the unique tree of its order with the least asymptotic lower three-uniform saturation coefficient, a/(2a + 1), and the unique minimizer for n ≥ 3(a + 1)(2a + 1); this is the Berge analogue of the theorem of Faudree, Faudree, Gould and Jacobson for graphs.
Details
- Year
- 2026
- Discipline
- Mathematics
- Area
- Extremal hypergraph theory
- Subject
- Graph theory and graph polynomials
- Result type
- Exact formula with a complete Lean proof and a minimality theorem among trees
- Formal proof
- Standalone Lean package
- Family
berge-subdivided-star- Keywords
- Berge hypergraphs, saturation numbers, trees, subdivided star, loose stars, uniform hypergraphs, extremal hypergraph theory
Statement and scope
Formal scope. Lean 4.35.0 proves, for actual r-uniform hypergraphs on Fin n, Berge copies of B_a with injective vertex and hyperedge maps, and saturation under every absent r-set, that the saturation number, defined as the least size of a saturated hypergraph on Fin n, equals ⌊a(n + 1)/((r − 1)a + 1)⌋ for all a, r ≥ 3 and n ≥ (r − 1)a + 1, together with the near-minimum structure theorem; a strict audit covers all 570 project declarations. The smaller orders, the sharpness constructions and the minimality among trees have conventional proofs.
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.pdf314 KB- PDF on GitHub
papers/mathematics/ berge-subdivided-star/ manuscript.pdf - LaTeX source
papers/mathematics/ berge-subdivided-star/ 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-subdivided-star/ - Lean project
papers/16 Lean filesmathematics/ berge-subdivided-star/ lean/ - Lakefile
papers/mathematics/ berge-subdivided-star/ 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-subdivided-star-verification- README
papers/mathematics/ berge-subdivided-star/ README.md - Verification guide
papers/mathematics/ berge-subdivided-star/ verification/ README.md - Verification record
papers/mathematics/ berge-subdivided-star/ VERIFICATION.md - Authorship
papers/mathematics/ berge-subdivided-star/ 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.03735. · Faudree, Faudree, Gould and Jacobson, Saturation numbers for trees, 2009. · English, Gerbner, Methuku and Tait, 2019.
Questions and answers
What is the Berge saturation number of the subdivided star?
For B_a, the star K_{1,a} with one edge subdivided, and all a, r ≥ 3 and n ≥ (r − 1)a + 1, the least number of hyperedges of an r-uniform Berge-B_a-saturated hypergraph on n vertices is ⌊a(n + 1)/((r − 1)a + 1)⌋. Disjoint loose stars with at least a spokes and fewer than r − 1 isolated vertices attain it; for smaller n the value is a or the number of all r-sets.
Which tree has the smallest Berge saturation number?
In three-uniform hypergraphs, for every a ≥ 5 the subdivided star B_a is the unique tree on a + 2 vertices with the least asymptotic lower saturation coefficient, a/(2a + 1); every other tree has coefficient at least (a + 1)/(2a + 3), and B_a is the unique minimizer for n ≥ 3(a + 1)(2a + 1). Faudree, Faudree, Gould and Jacobson proved the corresponding statement for graphs in 2009.
Is the result formally verified?
Partly. Lean 4 proves the exact formula in every uniformity, with the saturation number defined as a minimum over all hypergraphs on n labelled vertices, and the near-minimum structure theorem. The smaller orders, the sharpness constructions and the minimality among trees have conventional proofs in the manuscript.
Cite
Citation file papers/. For the whole collection, use CITATION.cff or CITATION.bib.
@misc{goyal2026bergesubdividedstar,
author = {Goyal, Dev D.},
title = {Exact {Berge} Saturation Numbers of the Subdivided Star in Every Uniformity and Its Minimality Among Trees},
year = {2026},
month = nov,
note = {Preprint. Fully autonomous agentic research; publication responsibility: Dev D. Goyal},
url = {https://github.com/dvgyl/math-and-theory/tree/main/papers/mathematics/berge-subdivided-star}
}