Math and TheorySharp escape of complex domination roots in square flowers
Problem and result
- Problem
- Largest complex domination roots of square flowers (n four-cycles sharing one vertex)
- Status
- New theorem
- Result
- For the square flower F_{4,n} of n four-cycles sharing one vertex, the largest domination-root modulus R_n satisfies R_n < 2 + √(4n/W(4n)) for all n ≥ 1 and 4n/R_n² = log(4n) − log log(4n) + o(1).
Abstract
Sharp complex-root escape for square flowers, with complete flower and book real-root classifications and multiplicities.
Details
- Year
- 2026
- Discipline
- Mathematics
- Area
- Graph polynomials
- Subject
- Graph theory and graph polynomials
- Result type
- Standalone theorem and reproducible proof package
- Formal proof
- Standalone Lean package
- Family
graph-roots- Keywords
- domination roots, domination polynomial, complex roots of graph polynomials, square flowers, book graphs
Statement and scope
Formal scope. All numbered manuscript conclusions are formalized in seventy modules with 258 endpoint audits. Historical novelty and exact external-source correspondence remain provisional.
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.pdf333 KB- PDF on GitHub
papers/mathematics/ graph-roots/ manuscript.pdf - LaTeX source
papers/mathematics/ graph-roots/ manuscript.tex - Bibliography
papers/mathematics/ graph-roots/ references.bib
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/ graph-roots/ - Lean project
papers/70 Lean filesmathematics/ graph-roots/ formalization/ - Lakefile
papers/mathematics/ graph-roots/ formalization/ lakefile.toml - Toolchain
leanprover/lean4:v4.19.0 - Library roots
Reproduce
The commands below are quoted from papers/, which gives their context and working directory.
Build and reproduce
set -e
mkdir -p build
pdflatex -interaction=nonstopmode -halt-on-error -output-directory=build manuscript.tex
bibtex build/manuscript
pdflatex -interaction=nonstopmode -halt-on-error -output-directory=build manuscript.tex
pdflatex -interaction=nonstopmode -halt-on-error -output-directory=build manuscript.tex
cp build/manuscript.pdf manuscript.pdfBuild and reproduce
python3 -B supplement/test_optimization_guard.py
python3 -B supplement/checks.py --max-n 20 --output build/replayed-checks.json- README
papers/mathematics/ graph-roots/ README.md - Proof map
papers/mathematics/ graph-roots/ PROOF_MAP.md - Authorship
papers/mathematics/ graph-roots/ AUTHORSHIP.md - Repository guide
verification/README.md - Unfinished proofs
UNFINISHED.md
Source and prior work
Prior work. The Omega Institute's public repository records a refutation of Rather's book-graph Conjecture 5.4 at n = 1, committed on 28 October 2026 (issue #23025), about 17 hours before my first commit. No priority is claimed for it. Priority and novelty record.
Questions and answers
How large can domination roots of square flowers be?
For the graph F_{4,n} of n four-cycles sharing one vertex, the preprint proves R_n < 2 + √(4n/W(4n)) for every n ≥ 1, with W the positive real Lambert function, and constructs actual complex roots giving 4n/R_n² = log(4n) − log log(4n) + o(1), so R_n ~ 2√(n/log n). This describes only the extremal root modulus, not a limiting curve for the whole zero set.
Is this related to earlier work on friendship and book graphs?
Domination polynomials of generalized friendship and book graphs were studied by Jahari and Alikhani and by Rather; the square flower differs from triangular friendship graphs and from book graphs, whose squares share an edge. The literature comparison is incomplete, so no conjecture-resolution or priority claim is made.
Is the proof formally verified?
Yes. The conclusions of all numbered results, including the escape theorem and the complete square-flower and book-graph real-root classifications, are formalized in 70 Lean 4 modules with 258 explicit statement checks; finite and numerical checks support but do not replace the proofs.
Does this settle Rather's book-graph root conjecture?
The companion proposition shows that the conjecture fails only at n = 1 and holds for every n ≥ 2. The n = 1 failure was recorded earlier in the Omega Institute's public repository, committed on 28 October 2026 (issue #23025); no priority is claimed for it.
Cite
Citation file papers/. For the whole collection, use CITATION.cff or CITATION.bib.
@unpublished{goyal2026squareflowerroots,
author = {Goyal, Dev D.},
title = {Sharp escape of complex domination roots in square flowers},
year = {2026},
month = oct,
note = {Unpublished manuscript, 28 October 2026. Complete conventional proofs; no completed Lean formalization or priority claim.}
}