The theorem under investigation
Let p be a complex polynomial of degree n ≥ 2 whose zeros lie in the closed unit disk. Sendov's conjecture says that, for every zero a of p, there is a critical point w such that
p′(w) = 0and|w − a| ≤ 1.
Revision 16 presents a self-contained computer-assisted proof candidate for this statement. “Self-contained” means that the manuscript includes the written reduction from a hypothetical counterexample to its two terminal scalar propositions; it does not mean that the entire argument has been formally verified.
What Revision 16 adds
Revision 16 is an audit-hardening successor to the self-contained Revision 15 manuscript. It keeps the same mathematical strategy and terminal certificate conclusions while making several supporting steps and release checks explicit:
- positivity and endpoint-continuity statements used by monotonicity and limiting arguments;
- the full Maclaurin-to-RMS normalization and exact tail comparisons;
- local feasibility guards in the finite-certificate generator;
- deterministic regeneration and byte comparison of the complete finite certificate;
- permanent mutation tests, a closed-world release manifest, and an exact proof-input manifest;
- restored historical framing, bibliography, and the Brown–Xiang low-degree overlap discussion.
The packet's audit-resolution note reports that the Revision 15 audits found no fatal or major mathematical error. That is retained review history, not an independent specialist certification of Sendov's conjecture.
Proof-candidate architecture
1. Normalize a hypothetical counterexample
The manuscript begins with a polynomial that would violate Sendov's conclusion and contracts it to a first-contact configuration. The distinguished zero, the other roots, and the critical points remain in controlled geometric regions while one critical point reaches the relevant distance-one boundary.
2. Encode the critical-point geometry
Reciprocal critical coordinates and an antiderivative factorization convert the geometry into coefficient identities. A product-defect estimate supplies the quantitative bridge used by the later scalar reduction.
3. Force one scalar parameter
A polar-product identity defines an explicit scalar parameter and derives a lower bound from the first-contact geometry. This avoids leaving the central parameter as an unspecified root of an auxiliary equation.
4. Reduce the obstruction
Integration by parts and Maclaurin's inequality transform the remaining high-degree obstruction into a one-variable demand. Degrees two through five are treated separately in the manuscript.
5. Establish incompatible inequalities
For m = n − 1, a counterexample would force
(m + 1) E_m(λ) > 1 + λ,
whereas the proposed master estimate supplies the reverse strict inequality throughout the feasible range.
6. Cover the finite and uniform ranges
The endpoint regime is handled analytically. The finite interval 5 ≤ m ≤ 499 is covered by an exact rational certificate, while the remaining large-degree regime uses a uniform analytic estimate supported by a second exact certificate.
Exact computational evidence
The accompanying packet retains exact rational certificate data, generators, primary verifiers, arithmetic cross-checks, mutation tests, reference logs, and manifests. Its expected summaries include:
- 16,862 finite certificate leaves, of which 16,367 are ordinary rational leaves and 495 are algebraic terminal slivers;
- 15,872 failing internal nodes retained during deterministic regeneration;
- 20,994 exact rational boxes in the uniform auxiliary certificate;
- 6,500 Bernstein-positivity checks;
- mutation controls that are rejected as expected.
The exact programs certify only the two terminal scalar propositions stated in the packet: the finite m = 5,…,499 inequality and the uniform auxiliary bound. They do not machine-check the barrier reduction, coefficient bridge, polar forcing, integration-by-parts argument, mismatch theorem, or analytic range estimates.
Reproducibility boundary
The paired arithmetic consumers are implementation cross-checks of shared mathematical specifications. They are not specification-independent proofs of the complete theorem, and there is currently no Lean or other proof-assistant formalization of the full manuscript.
The packet README also records a release limitation: the included PDF was built with Tectonic with its references resolved, while the retained logs/latex_compile.log belongs to the immediately preceding Revision 16 source state because the recorded pdfTeX binary was unavailable. The mathematical PDF, matching TeX source, exact certificate inputs, and other retained checks are fixed here byte-for-byte; the stale reference-build log should not be described as a replay of the final TeX bytes.
The README mentions a detached ZIP checksum intended to be distributed beside the archive. No detached checksum file was supplied to ProofAtlas; this page instead records and audits the ZIP's SHA-256 directly.
Authorship and AI disclosure
Lech Mazur is the author and takes responsibility for the manuscript. The manuscript reports substantial OpenAI GPT-5.6 Pro involvement in mathematical exploration, proof development, computation, adversarial auditing, and exposition, with human orchestration and reconciliation.
Public revision and preserved history
This page hosts public Revision 16, dated August 3, 2026, with release identifier SENDOV-REV16-SELF-CONTAINED-2026-08-03. The PDF, matching TeX source, and complete ZIP packet are fixed, digest-bound copies.
Public Revision 14 remains available at its original page. It has not been replaced or redirected. Future corrections should likewise receive new immutable versioned pages and file routes.
Current status
This remains a proof candidate, not an accepted ProofAtlas proof or a formally verified resolution of Sendov's conjecture. Its substantial exact computation and audit history make it suitable for close examination, but independent specialist assessment of the written analytic reduction remains important.