The polynomial basis · V0
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 v1.3 · 26 October 2026. V2o proves that the parent profile and binomial summaries δ₁…δd suffice for a factor of degree ≤ d, and that monomial-factor responses determine these summaries over characteristic-zero fields. At Table 3 piece (6,3), 157 of 2,361 factor multisets now have certified profiles. Mac and Linux certificate builds passed (3,663 jobs each), and the eight-statement V2o Comparator suite was accepted by the Linux Lean default kernel. The remaining rational moments and full Gram matrices await certification.
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 · V2c
General monomial formulas for I T , with arbitrary cap functions and a worked exact rational Gram entry.
Marginal-fibre geometry · V2d
The exact piecewise fibre endpoint for J T , empty-fibre theorems, marginal identity, and inner polynomial integral, independently verified on the VPS.
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 J T .
Exact marginal Gram entry · V2f
All endpoint branches integrated and assembled: the constant-generator entry J T [1,1] ≈ 1.1193487646 × 10⁻⁵⁵, certified exactly from 133 rational pieces.
Bilinear power-sum Gram entry · V2g
The first nonconstant marginal entry J T [P₂,1] ≈ 4.99943968764 × 10⁻⁵⁷, certified using 133 rational pieces and 266 exact lemmas. Coordinate placement and shifted power sums are formalized.
Power-sum-square Gram entry · V2h
The diagonal entry J T [P₂,P₂] ≈ 2.27107 × 10⁻⁵⁸ completes the 2×2 block. Two-coordinate placements, diagonal terms, and shared moment-table certificates are verified by Lean.
General marginal Gram entries · V2i
For arbitrary generators G a,λ = (L − P₁) a P λ , Lean proves a rational marginal Gram-entry representation. The Table 3 theorem covers every generator pair in B₂₁; selected entries are evaluated with exact certificates.
Shared-moment aggregation · V2j
Canonical moment keys collect repeated contributions across Gram-entry combinations. Lean proves the aggregation agrees exactly with V2i, with four compiled demonstrations and a 24-statement Comparator accepted independently on the MacBook Pro and Linux VPS.
Symmetric-function reduction · V2k
A canonical augmented-monomial symmetric-function evaluator replaces V2i’s placement recursion. Lean proves general equivalence with V2i’s placement recursion and verifies exact coefficient tables, including an 85-coefficient piece demonstration. Its 36-statement Comparator suite was accepted on Mac and Linux VPS.
Staged symmetric-function certificates · V2ℓ
Lean proves that certified step chains, chunks, and merges recover V2k’s evaluator and V2i’s placement value. Factor-order invariance permits prefix reuse; certified profiles give a 231-moment representation for the degree-12 Table 3 piece (6,3). The 35-statement Comparator passed on the Linux VPS.
Certified prefix-trie evaluation · V2m
Lean certifies 77 nonroot prefix-trie nodes and 78 reusable moment profiles, with equality to V2i’s placement evaluation for arbitrary moment oracles. Kernel-checked degree-40 coefficient tables include one Table 3 piece (6,3); the remaining rational moments and trie nodes are future work. The 20-statement Comparator passed independently on the Linux VPS.
Direct marked-profile transitions · V2n
Ordinary profiles alone are insufficient for continuing shifted power-sum transitions; a higher-order marked profile is sufficient, with equality tested against every function on marked keys. On Table 3 piece (6,3), Lean certifies 34 direct nodes, including 25 new factor multisets, and covers all 52 multisets in the |λ| ≤ 8 block. Two coefficient tables each use 489 moment keys. The 19-statement Comparator passed on Linux.
What one factor reads · V2o
For factors of degree ≤ d, Lean proves that the parent profile plus binomial summaries δ₁…δ d suffice; monomial-factor responses determine these summaries in characteristic zero. One-level certificates cover 66 three-factor multisets of degree ≤ 26 at Table 3 piece (6,3), forming no canonical leaf states. Combined V2m–V2o coverage is 157 of 2,361 multisets at that piece, with a 574-key coefficient table and Linux acceptance of the eight-statement Comparator.
Bounded prime gaps
Combinatorial packing and the verified conditional implication from DHL[45,2] to H 1 ≤ 212; additional analytic and variational obligations remain.
02 / Verified mathematics
A verified implication and its research pathway
DHL[45,2] ⟹
H
1
≤ 212
Lean-verified implication under the stated DHL[45,2] hypothesis.
V2f–V2h certify the symmetric 2×2 marginal Gram block on {1, P₂}. V2i gives exact rational representations for every B₂₁ generator pair; V2j–V2m develop shared moments, symmetric-function evaluation, staged certificates, and prefix-trie reuse. V2n certifies direct marked-profile transitions. V2o proves which binomial read summaries suffice and are determined by degree-bounded monomial responses, adding 66 one-level three-factor certificates. Together V2m–V2o certify 157 of 2,361 factor-multiset profiles at the specified Table 3 piece. Exact rational moments, the full 846×846 matrices, optimized polynomial P⋆, and variational positivity remain outstanding.
03 / Exact marginal Gram block
Three certified entries, one polynomial pair
For the functions 1 and P₂ = ∑ᵢxᵢ², the marginal bilinear form has a rational 2×2 Gram block. Decimal values below are readable approximations of the exact rational certificates.
G
J
on (1, P₂)
1.11935 × 10
−55
4.99944 × 10
−57
4.99944 × 10
−57
2.27107 × 10
−58
The numerical Cauchy–Schwarz ratio J
T
[P₂,1]² / (J
T
[1,1] · J
T
[P₂,P₂]) ≈ 0.984. The matrix entries are certified individually; a separate exact determinant-positivity certificate is a further target.
V2h handles diagonal and distinct-coordinate placements. V2i generalizes the placement construction to products of arbitrary power sums and certifies further Table 3 entries: JT[P₄,1] ≈ 2.75169 × 10−59, JT[P₍₂,₂₎ (= P₂²),1] ≈ 2.28799 × 10−58, and JT[L−P₁,1] ≈ 5.52809 × 10−57. These approximations correspond to exact rationals in the Lean certificates.
04 / Proof blueprint
Follow the mathematical dependencies
This theorem map follows the mathematical dependencies from established proofs to current research. Its next iteration will connect Lean declarations, mathematical statements, dependencies, and kernel verification logs.
05 / Reproducibility
Readable mathematics, checkable evidence
Reproducible Challenge/Solution pairs, pinned dependencies, generators and per-release result YAML files document the proof chain. Comparator acceptances below are independent checks of the named statements; Mac results marked “Build only” do not imply a Mac Comparator pass.
| Release | Statements | Mac | Linux VPS | Record |
|---|---|---|---|---|
| V2i | 33 | Comparator passed | Comparator passed | YAML |
| V2j | 24 | Comparator passed* | Comparator passed | YAML |
| V2k | 36 | Comparator passed | Comparator passed | YAML |
| V2ℓ | 35 | Build passed; Comparator unconfirmed | Comparator passed | YAML |
| V2m | 20 | Build passed; Comparator unconfirmed | Comparator passed | YAML |
| V2n | 19 | Build passed; Comparator unconfirmed | Comparator passed | YAML |
| V2o | 8 | Build passed; Comparator unconfirmed | Comparator passed | YAML |
* Mac Comparator used a non-isolating development substitute for Linux landrun where specified. For V2ℓ–V2o, “Build passed” denotes successful macOS certificate builds rather than macOS Comparator acceptance. Linux Comparator checks used real landrun. V2o: proof commit 89b43fa, verification record f779ea7, merge 6a51ba9; both sequential certificate builds passed (3,663 jobs), and the eight-statement suite was accepted as one Comparator run by the Linux Lean default kernel. These certificates establish coefficient representations, not evaluated rational moments or positivity.
This independent Lean formalization builds on the mathematical argument in Axiom Math's bounded-prime-gap research . The repository records our statements, proof terms, certificates, and verification provenance.