Internal proof audit

September 9, 2026. Review by the originating Codex agent. No separate-agent review or human referee review is claimed.

General arguments checked

1. Integer approximation. Rounding the unnormalized Bernstein coefficients preserves integer polynomial coefficients. The two endpoint coefficients are exact integers. Every interior binomial coefficient is at least the degree, giving a uniform rounding error at most one over twice the degree. Together with Bernstein approximation this proves the needed density statement.

2. Positive coefficients and finite trees. Endpoint zeros are factored before the eventual positivity argument; a positive minimum is used only for the remaining factor on the closed interval. The falling-factorial coefficient formula has a uniform error for fixed polynomial degree. Unnormalized Bernstein coefficients of an integer polynomial are integers. For a partition summing to one, each coefficient column sums to the exact number of leaves of the corresponding binary-tree weight. Thus the construction uses finite trees with valid integer label counts.

3. Weighted lifting. The cutoff is identically zero in neighborhoods of every zero of the denominator, including both endpoints. The quotient therefore extends continuously, with the chosen integer endpoint values. Transitions occur only where the original function lies strictly inside the required bounds. Positive linear endpoint margins and compactness give a global margin proportional to t(1−t). The approximation perturbation contains the same factor, so a sufficiently small uniform error preserves strict inequalities throughout the open interval. Real repeated roots cause no additional issue because whole neighborhoods are removed from the quotient.

4. Endpoint arithmetic. Integer linear corrections realize the two endpoint residues simultaneously. Subsequent corrections divisible by X(1−X) preserve those values and change the endpoint derivatives independently by nonzero integer moduli. Both signs at both endpoints were checked. In the finite-generation argument the derivative must also lie below the derivative of the upper bound; choosing a larger integer N gives an open interval containing a representative of every residue class.

5. Arithmetic classification. Monicity identifies the evaluation kernel with the principal polynomial ideal over the integers. Reduction modulo the two endpoint ideals is exactly evaluation modulo the two endpoint values of the minimal polynomial. The identity embedding is included when the parameter itself is in the open unit interval. Values zero and one are separately admitted. These points avoid imposing a maximal-order hypothesis or confusing a finite-expression set with its topological closure.

6. Discreteness. The non-strong-PV algebraic case has at least one unused real Minkowski dimension. Increasing a box in those dimensions makes its volume arbitrarily large while physical coordinates remain arbitrarily small and internal coordinates remain bounded by a fixed admissible margin. The resulting nonzero ideal elements approach zero physically. Injectivity of the field embedding ensures they are nonzero there. Translating by λ(1−λ) gives actual accumulation within the membership set. The converse uses the full lattice and a compact difference window. The interval parameters and the degenerate endpoints are handled separately. Discreteness implies algebraic integrality by the explicitly cited external theorem.

7. Projection density and the model set. The trace pairing identifies the full dual lattice with a lattice of field elements, including complex coordinates with the factor two and no accidental conjugation. A character annihilating a proper projection would give a dual field element with a zero omitted embedding, which is impossible unless it is zero. Every finite residue class consequently has dense internal image. The endpoint ideals are comaximal and their product has the stated index. Boundary internal coordinates force the field element to be zero or one. Relative density is proved using compact representatives and a finite open cover. Uniform separation of the difference set uses a difference of two differences, hence four copies of the compact window, not merely two.

8. Finite generation. Representatives of every endpoint-ideal class exist in the cube by projection density. They form one fixed finite seed. For each target, the two endpoint representatives may be different. Large powers of X and 1−X make their internal contribution small. Weighted lifting provides two remaining positive integer polynomials; all four sum to one and evaluate to the target. The finite-tree lemma then proves membership in the closure of this fixed seed. The degree can depend on the target; no uniform tree-depth claim is inferred.

Finite checks and limits

The standard-library checker records 1,008 exact Bernstein reconstruction/evaluation checks, 1,599 rational rounding-bound checks, and 1,464 endpoint derivative-residue checks. It recovers precisely the four published quadratic equality pairs in the tested parameter range. Exact cubic sign changes and the rational-root exclusion support the example. Bounded closure calculations for i, 2i, and 3i obey the congruences and reach every predicted point in the stated inner box; no global absence is inferred from a bounded calculation.

These checks are consistency evidence. The all-degree statements depend on the general proofs above, not on extrapolation from finite data. The source theorem establishing algebraic integrality is a cited external dependency, not an independently certified calculation. All nine pages of the final PDF were rendered and visually inspected. Full Markdown conversion preserved source math and theorem/proof structure; its mathematical expressions passed the local renderer check. Live GitHub Markdown rendering was not separately inspected.

Admission decision

No unresolved mathematical step was identified in the internal audit of the manuscript's stated claims. Publish as one complete proposed solution with the accompanying source assessment and explicit preparation disclosure. Public hosting does not certify historical priority or replace expert review. The global count of significant verified solutions remains distinct from the number of public manuscripts.