The first pursuit: a computational and formal attack on the structure around the Riemann hypothesis. Two arms run side by side, and neither is allowed to vouch for the other.
| 380 | theorems |
| 45 | lemmas |
| 0 | sorrys |
| 158 | definitions |
| 45 | Lean modules |
| 10,463 | Lean lines |
A sorry is a hole left in a proof, and Lean will happily accept
a file full of them. This arm has none, which is why its declarations are called
theorems here without qualification.
| module | decls | subject | |
|---|---|---|---|
| DHAnalytic | 33 | The analytic half of the Davenport-Heilbronn theorem | |
| MatchingCount | 32 | Exact labelled matching counts | |
| DHCertSupport | 31 | Support layer for the generated rung-3 certificate | |
| HigherXi | 27 | Kernel-checked algebra for the URMS2-051 witness | |
| IntervalCExp | 26 | Certified complex exp, and the Dirichlet term n^{-s} | |
| SupportSizeMajorant | 20 | Arithmetic support-size majorants | |
| PowerfulDecomposition | 19 | Powerful-squarefree arithmetic decomposition | |
| LogMeanValue | 18 | Logarithmic-frequency mean-value bounds | |
| IntervalExp | 17 | Certified interval exp and log | |
| TwoRangeWeights | 15 | The exact two-range weights at sigma = 3/2 | |
| AristotleRAMS2 | 13 | Exact partial summation and the RC2 endpoint energy | |
| Rigor | 13 | Certified Interval Evaluation |
DH_demo_ne_zero: the Davenport-Heilbronn function is non-zero
at 3/2 + 3i, kernel-checked with no oracle input. The
pipeline closes end to end: rational interval arithmetic, certified
transcendentals, contour criterion.
That function shares ζ's functional equation, has real coefficients and a real Hardy-style Z, and violates the Riemann hypothesis. Every structural claim here is run against it first. A property it also has has explained nothing.
| count | ||
|---|---|---|
| core modules | 25 | ζ, zeros, explicit formula, heat flow, Weil, rigor, Li, criteria |
| core lines | 21,164 | arbitrary precision throughout; mp.dps set explicitly |
| public functions | 311 | counted from the module ASTs, not a maintained list |
| tests | 1,783 | across 68 files |
| test lines | 31,563 | more test code than core code, which is the intended ratio |
| ball-arithmetic backends | 2 | Arb and mpmath, each checking the other |
Identities are exposed as measured defect functions rather than assumed, and the suite checks itself against mpmath's oracles rather than its own arithmetic. With one interval backend installed the cross-check is absent, and the suite says so instead of passing quietly.
certified: True is
asserting a theorem. If any step silently falls back to floats, that is a
critical defect and not a rounding detail.Kept with the mechanism that broke each one, and the test that now catches it.
the construction used u u* where the pinned upstream zero side uses u u^T; an off-line pair is the hyperbolic block 2m(xx^T - yy^T), whose interaction with the on-line part can be negative, and the proposed final additive inequality reads 9 >= 13
midpoint bin-to-cell assignment inflated chain counts, briefly producing a conditional bound past CG 1993
individual place contributions can sometimes be represented as norms, but the local pieces do not consistently carry the sign naive global assembly needs
Clone it, install it, run the suite; every claim on this site is one you can re-derive. The Lean arm builds under a proof kernel that rejects anything unfinished. Continuous integration runs the fast tier on every push and the whole thing nightly, so the tree is green because it is green rather than because someone remembered to look. Start with the reading course.