[subfish-zhou]

Updated scope: verified first-origin and centered extensions

The existing degree-uniform scalar endgame is retained for the remaining region. This update additionally formalizes the locally obtained analytic results and wires the new first-origin routes into both final conjecture proofs.

Main additions

• Raw polar implies the direct integral budget D for every natural m ≥ 256 and all 0 < a < 1, with closed −1 ≤ x ≤ 1. This theorem does not assume an alpha cap, centroid identity, second-origin identity, or the desired analytic estimates. See Sendov.PaperUniform.uniform_D.
• For all m ≥ 7 with m(1-a) ≤ 2/5, prove the quantitative gap B−T > (1-a)/1000. Stronger historical margins and rate estimates are preserved separately.
• Interior now uses first-origin alone at n=6,7; for all n≥257; and in the near-endpoint subregion of 8≤n≤256. The remaining finite region still uses the existing endgame. Full m≥7 all-radius D is not claimed.
• Add averaged-second-moment boundary rigidity, real-split collinear moment results, complete finite complex centered expansions/coefficient majorants/C-budget, curvature secant gates, and exact full-polar diagnostic certificates. The real-split strengthening is independent of the general complex Solution proof.
• The two final public statements, strict/interior and equality alternatives, and Lean/Mathlib pins are unchanged. Mathematical sources and original attributions are retained; restoring Tao's stronger rational polar bound is reuse, not a discovery claim.

Verified scope and limitations

The acceptance inventory covers 92 normalized locally obtained result families, including actual exported Lean versions of 21 former corollary recipes. This is not a count of 92 atomic declarations. Three previously heuristic asymptotic groups are explicitly classified as unproved calculations; downloaded third-party proofs are not silently included. See scope.

Local exact-source verification completed 97 module compilations + 96 Lean kernel replays (193 successful checks). The import-only Sendov umbrella has no local declarations; it is compiled, and declaration-bearing modules are replayed separately. 243 named audit roots use only propext, Classical.choice, and Quot.sound. Ten frozen boundary/final contracts remain equal. Both generators reproduce their eight outputs byte-for-byte. These local checks are not a claim of passed GitHub CI, nor a fresh replay of all Mathlib.

This is added mathematical coverage, not a net compression or speedup: relative to the previous PR snapshot 0a4e966, production Lean grows by 7,887 lines. Shared-host cached-import measurements put Interior at about 3.50s before versus 7.37s after. No upstream performance claim is made.

Current review and replay material

• Final report
• Actual verification counts and command receipts
• Full-D semantic review and exact diagnostic binding review
• In-repository bounded replay driver, using an explicitly supplied pinned environment configuration and private project objects

New experiments on the remaining domain will be kept separate until proved and checked. This update does not claim a solution of the residual full-D or global C-near problems.

Previous PR baseline and its validation (historical, through 0a4e966)

Summary

This replaces the degree-specific certificate endgame with a scalar bound on the complete legal real-degree domain:

[
m\ge5,\qquad 0<\alpha\le17,\qquad 2\alpha\le m
\quad\Longrightarrow\quad H_m(\alpha;e(\alpha))<1,
]

where m=n-1, e(alpha)=u-u^3/30, and u=alpha/(alpha+3). The theorem is Sendov.distillScalar_lt_one_real. The definitions and proof-reading guide are in the mathematical note.

The construction retains the Mazur–Tao reduction and adopts Senjian An's cubic envelope and two-chord estimates.1 Its principal change is to retain same-alpha information while controlling complete degree rays, rather than use a finite degree table followed by a separate tail. Local contribution: subfish-zhou. Original mathematical attributions and license notices are retained.

This is not certificate-free: the three alpha regions still use fixed positivity identities of degrees 53/47/47, with 150 main coefficients and 71 homogeneous-factor coefficients. No smallest-threshold, optimality, first-solution, or universally easier-hand-calculation claim is intended. The later 9/9/18 experiment is not included.

What changes, and what does not

• Solution.lean, Challenge.lean, and comparator.json are unchanged from the review base. The final Sendov and Phelps–Rodriguez statements, including the equality classification, are preserved. Lean and Mathlib pins are unchanged.
• Small, middle and large alpha regions cover the full real domain, including the legal m=2*alpha endpoint. The raw totalized value at alpha=0 remains separate from continuous extension.
• The obsolete R/FiniteRange/LargeDegree route and its specialized generators are retired. There is one active proof route, not a compatibility copy of both endgames.
• Intermediate API change: Sendov.polar_origin_incompatible now requires 6 <= n, rather than upstream's 5 <= n. Degree five is handled by the existing polynomial low-degree argument in Interior. This preserves the final conjecture statements, not the old standalone scalar API at degree five. Downstream use of retired helpers needs migration.
• This accumulated diff also includes local proof simplifications, generator portability/atomic-write fixes, audit improvements, tests, and documentation updates. These are supporting engineering changes, not additional mathematical discoveries. The CI workflow change is a comment update; visible CI remains build plus trust audit.

The original production history remains available at the fixed upstream source tree, including its making-of document. The local automation does not replace attribution of that work. The existing acknowledgement of Pickhardt's mean/variance-budget influence is retained without asserting an unverified priority claim.

Review material

• Mathematical note: theorem, inherited inputs, argument structure and limitations. It is a review guide, not a standalone paper.
• Complete coefficient data.
• Independent exact-arithmetic replay and its local result: reconstruct all three complete identities and 18 factor identities; reject an interior-coefficient mutation in each main identity. This check does not replace the analytic lemmas or Lean's kernel.

Suggested Lean reading order: Reduction/CubicScalar → Common/DistillationBounds → the small/middle-alpha modules → DistillationCorrelatedPeak and DistillationPeakRational → PeakAlgebra, PeakFirst/PeakRest, PeakClosure. Shared budget placement keeps the two heavy complementary certificates independent in the build DAG.

Validation

Existing local evidence for mathematical source c7f25171a07b916a678b0df1dbd32ee55eb5e4df:

• Six fresh-project-object builds in each of the final two validation rounds, using the pinned external dependencies.
• Full replay of 47 proof-bearing modules at the mathematical milestone; subsequent exact replay of the 14 affected modules, with unchanged modules retaining that prior evidence.
• 16 Python tests, 13 Lean test/audit source checks in the final round, and complete four-root proof-value traversal with 32 positive-consumption checks.
• 386 original strict declaration comparisons plus three explicit numeral-Prop supplements, not 389 strict passes. For S, denominator2, and gap1, automatic proof-sharing names changed; the supplemental check verified the identical concrete Prop types/proofs and full expressions after only those reference expansions. Original strict failures were retained, with ten negative controls and independent review.
• Only the standard propext, Classical.choice, and Quot.sound proof axioms. The two unchanged Challenge.lean specification holes are not proof dependencies.

The publication follow-up changes only the accompanying review material and a license-copy trailing blank line; the Lean proof sources, dependencies and CI are unchanged from that validated source snapshot. Its exact-arithmetic note replay has been run. Local results above are not a claim that remote CI has already passed, and no local-round timing is presented as an upstream speedup.

Portable commands are in the repository verification guide. The basic sequence is:

lake exe cache get
lake build
sh scripts/audit.sh
lake env lean tests/NoFiniteRows.lean

The documented Python regressions require SymPy; the independent kernel loop and all Lean probes are separate checks. The original-object declaration-comparison supplement requires its historical old/new objects and is not reproduced by these four commands alone.

Maintainer review

I would particularly welcome feedback on the intermediate-API migration, the attribution, and the trade-off between a uniform degree argument and fixed alpha certificates. If a narrower review surface is preferred, the independent engineering changes can be discussed separately from the mathematical replacement, without retaining a dead second endgame indefinitely.