rh_certificate
plain-language theorem explainer
rh_certificate shows that the Riemann hypothesis follows once the Recognition Science physical thesis is assumed for zeta zeros. A researcher bridging analytic number theory to the T0-T8 chain would cite it to obtain the critical-line location. The proof is a direct term application of the fuller derivation that splits cases on the real part and invokes the functional equation for the left half-plane.
Claim. If every nontrivial zero $ρ$ of $ζ(s)$ in the open strip $1/2 < Re(ρ) < 1$ corresponds to a physical recognition event on the arithmetic ledger, then all nontrivial zeros satisfy $Re(ρ) = 1/2$.
background
The Zeta-Ledger Bridge module closes the formalization gap between the abstract DefectSensor and PhysicallyExists framework proved in UnifiedRH and Mathlib's concrete riemannZeta. Central definitions include the ontological dichotomy (a sensor has charge zero if and only if it physically exists) and RSPhysicalThesis, which asserts that every nontrivial zero in the open strip is a physical ledger event via the zetaDefectSensor construction.
proof idea
The declaration is a one-line wrapper that applies the fuller derivation in the same module. That derivation introduces an arbitrary zero s, performs a case split on whether its real part exceeds 1/2, invokes the right-half lemma using the thesis together with the dichotomy and de la Vallée-Poussin region, and reduces the left half via the completed zeta functional equation.
why it matters
rh_certificate supplies the main bridge from the physical thesis to the Riemann hypothesis, which is then used in rh_full and riemann_hypothesis_from_rs. It completes the argument that the hypothesis follows from T1 annular coercivity and the ontological dichotomy inside the T0-T8 forcing chain, with zero additional axioms beyond the thesis hypothesis itself. It leaves open whether the physical thesis admits a mechanical derivation from the ledger axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.