Proof Distillation for Sendov's Conjecture

From Computer-Assisted Analysis to a Hand-Checkable Proof

This repository contains the manuscript, figures, exact-arithmetic verification scripts, and reproducibility material for the paper.

Status: public preprint / research release. The manuscript may receive further revision before journal or arXiv submission.

Paper

• Compiled PDF
• LaTeX source

Main idea

The paper studies the final scalar inequality arising from the Mazur--Tao reduction of Sendov's conjecture. The proof is organized as a proof distillation:

1. replace a piecewise auxiliary bound by a smooth rational envelope;
2. majorize the scalar obstruction by an elementary term plus three positive components;
3. factor each component into monotone increasing and decreasing pieces;
4. reduce its critical-point equation to a polynomial of degree at most 7, 7, or 4, independently of the degree parameter;
5. replace optimization by rational root isolation and use mixed-endpoint bounds to estimate unknown interior maxima.

The main worked example is m=46, where the proof can be followed using rational root brackets and elementary inequalities.

Repository layout

.
├── paper/                 # manuscript, compiled PDF, figures, finite table
├── verification/          # exact and symbolic verification scripts + data
├── tools/                 # scripts used to regenerate illustrative figures
├── .github/workflows/     # automatic verification on GitHub
├── CITATION.cff           # citation metadata for GitHub's “Cite this repository” UI
├── requirements.txt       # optional Python packages for symbolic checks/figures
└── README.md

Verify the finite proof data

The two main checks use only the Python standard library:

cd verification
python verify_paper.py
python verify_hand_examples.py

Optional symbolic/expository checks require SymPy:

python -m pip install -r ../requirements.txt
python symbolic_checks.py
python rewrite_checks.py
python verify_expository_lemmas.py

On Windows PowerShell, elapsed time can be shown with:

cd verification
Measure-Command { python verify_paper.py }
Measure-Command { python verify_hand_examples.py }
Measure-Command { python symbolic_checks.py }
Measure-Command { python rewrite_checks.py }
Measure-Command { python verify_expository_lemmas.py }

The verification material audits the printed finite-degree table, worked examples, algebraic identities, the 7,7,4 critical-polynomial reduction, the Maclaurin coefficient certificate, and the two-chord identities. It is not a formal proof-assistant verification.

Compile the paper

From the paper/ directory, run pdfLaTeX twice:

cd paper
pdflatex -interaction=nonstopmode -halt-on-error Proof_Distillation_for_Sendovs_Conjecture.tex
pdflatex -interaction=nonstopmode -halt-on-error Proof_Distillation_for_Sendovs_Conjecture.tex

The bibliography is embedded in the LaTeX source, so BibTeX is not required.

Reproduce the figures

The figures are illustrative and are not proof premises. To regenerate them, install the optional requirements and run the figure script from tools/ after setting its output directory to paper/, or use the released vector PDFs already stored in paper/.

AI-assisted research declaration

The manuscript contains the full declaration. In summary, ChatGPT was used extensively as a research-assistance tool for exploratory numerical analysis, candidate inequalities and proof decompositions, symbolic/algebraic calculations, exact-arithmetic verification scripts, figures, and manuscript drafting/revision. The final mathematical statements and arguments were examined and verified by the author, and responsibility for correctness rests with the author.

Citation

GitHub should detect CITATION.cff and display a Cite this repository option. The citation metadata can be updated later if the paper receives an arXiv identifier, DOI, journal reference, or a new version number.

License

The manuscript, figures, and documentation in this repository are licensed under the Creative Commons Attribution 4.0 International License (CC BY 4.0).

The verification scripts and other source code are licensed under the MIT License.

See LICENSE-PAPER and LICENSE-CODE for details.

Reproducibility note

The numerical exploration that guided the proof is not required to check the final analytic argument. The repository preserves explicit rational brackets, finite tables, and exact/symbolic audit scripts so that the computationally discovered proof architecture can be inspected independently.