The package has three complementary levels of evidence. They answer different questions, and the final claims retain those distinctions.
| Evidence | What it establishes | Scope of the final release |
|---|---|---|
| Lean theorem | The precise formal statement follows from its recorded dependencies and the accepted foundational axioms. | The completed Nishibuchi conjecture, earlier Paper IX theory, and the inherited rank-four ordinary-step, sharp-period, and isometry results; see the Lean guide for build provenance. |
| Algebraic proof and audit | A universal mathematical result, subject to the written proof and its stated inputs. | The new general prime-power transfer, mixed-step and factorial gains, exact higher-order families, broader dyadic metric laws, and radius results. |
| Exact computation | The implemented assertion holds in its recorded finite domain, or an exact counterexample refutes an extension. | Coefficient regressions, period illustrations, and sharpness or cancellation checks. |
The generic theorem uses the integral Hurwitz-series product and reciprocal induction. The factorial theorem uses divided powers and explicit transforms of the ordinary Euler and Bernoulli series. The ordinary Euler arithmetic input is the classical Frobenius congruence, with normalization checked against Gessel's primary exposition. Address two has a self-contained central-factorial Bernoulli argument; addresses one and three use the proved tangent and cotangent transfers.
The broad exact regression through row \(512\) contains more than \(1.8\) million bounded difference assertions. Smaller later runs test the strengthened address-two filtration and the exact mixed parity law. Their manifests pin precision, coefficient definitions, input versions, and executed ranges.
The figures in this guide have a separate reproducibility record: sources/generate_figures.py, figures/exact_figure_data.json, and figures/figure_manifest.json. Its exact assertions validate the illustration data; theorem-derived curves are explicitly recorded as such.
The new general transfer, mixed-step, factorial, and analytic extension has not been newly formalized in Lean. The rank-four ordinary-step and sharp-period results have inherited Lean coverage, as mapped in the companion. Mathematical audits in this package are internal reviews, not claims of external peer review.