The polynomial basis
The 846-dimensional B₂₁ basis, with polynomial generators built from a slack power and power-sum factors.
Mathematics · Lean 4 · exact certificates
Exact Rational Integration over Constrained Simplices
Symmetric polynomial bases, explicit marginal geometry, and reproducible formal verification, developed through the study of bounded gaps between primes.
Draft v0.4 is available as a PDF. An interactive theorem-level blueprint remains in development. The published results do not constitute an unconditional Lean proof of the 212 bound.
01 / Mathematical objects
From constraints to exact integrals
The development specifies constrained simplex supports and piecewise cap conditions, constructs a rational polynomial basis, and derives exact integral formulas. The results are formalized in Lean 4 with explicit theorem dependencies and independently checkable certificates.
Exact integration
General monomial formulas for IT, with arbitrary cap functions and a worked exact rational Gram entry.
Two-aggregate integration · V2e-A
Weighted high-dimensional simplex integrals reduce to two aggregate variables. Rational polynomial forms and a worked certificate of 19/7680 are kernel-checked.
Polygon-cell integration · V2e-B
Exact rational polynomial integrals over clipped two-aggregate cells, with a verified cap-branch formula and a Table 3 certificate for one specified contribution to JT.
Exact marginal Gram entry · V2f
All endpoint branches integrated and assembled: the constant-generator entry JT[1,1] ≈ 1.1193487646 × 10⁻⁵⁵, certified exactly from 133 rational pieces.
Marginal-fibre geometry
The exact piecewise fibre endpoint for JT, empty-fibre theorems, marginal identity, and inner polynomial integral, independently verified on the VPS.
Bounded prime gaps
Combinatorial packing and the verified conditional implication from DHL[45,2] to H1 ≤ 212; additional analytic and variational obligations remain.
02 / A precise distinction
The conditional theorem and its open inputs
DHL[45,2] ⟹ H1 ≤ 212Formalized conditional implication, not yet an unconditional formalization of the bound.
The ongoing variational work supplies exact integral foundations. The constant-generator JT entry is now certified across all endpoint branches. Entries involving power sums, an optimized polynomial positivity certificate, and remaining analytic hypotheses are separate proof obligations.
03 / Proof blueprint
Follow the mathematical dependencies
This initial theorem map summarizes the stages. A later interactive edition will link individual Lean declarations, mathematical statements, dependencies, and kernel verification logs.
04 / Reproducibility
Readable mathematics, checkable evidence
Proof statements and certificates are preserved in the public repository with Challenge/Solution pairs, Comparator configurations, positive and negative controls, pinned toolchain information, and result records. All 18 Comparator suites were accepted in the VPS verification run, including V2f's exact first marginal Gram entry. The 133 rational certificate pieces were regenerated byte-for-byte; four positive Lean-file controls were accepted and five negative Lean-file controls rejected. The separate statement-mismatch control was tested by Claude on a fresh clone. The V2f proof is published at commit 8c50fb6 and its VPS verification provenance at da0c3fd.
The mathematical inspiration and bounded-prime-gap target are credited to the underlying research, including Axiom Math's original project. This is an independent formalization effort, not an Axiom Math publication or endorsement.