strip_zero_gives_nonphysical_sensor
plain-language theorem explainer
A zero of the Riemann zeta function at a complex point whose real part lies strictly between one half and one yields a defect sensor with nonzero charge that cannot be physically realized. Researchers deriving the Riemann hypothesis from Recognition Science cite this link between arithmetic zeros and non-physical ledger defects. The argument is a direct term that assembles the sensor from the real-part interval and unit charge then invokes the nonzero-charge and non-physicality facts.
Claim. Assume the Riemann zeta function vanishes at a complex number whose real part lies strictly between one half and one. Then there exists a defect sensor centered at that real part whose charge is nonzero and which fails to be physically realizable.
background
The Zeta-Ledger Bridge module closes the gap between Mathlib's riemannZeta and the DefectSensor framework proved in UnifiedRH. The central prior result is the ontological dichotomy: a sensor is physically realizable precisely when its charge vanishes. Defect sensors are constructed from real-part data in the open strip via the zeta defect sensor constructor, which encodes a meromorphic order witness at the given real part together with a charge parameter.
proof idea
The proof is a one-line term that applies the zetaDefectSensor constructor to the real part of the zero together with the open interval bounds and unit charge, then pairs the resulting sensor with the lemma establishing nonzero charge for that sensor and the lemma showing that the unit-charge sensor in the strip is not physically realizable.
why it matters
This theorem supplies the contradiction step inside the RS Physical Thesis, the single non-mechanical ingredient of the Recognition Science argument for the Riemann hypothesis. The thesis asserts that every nontrivial zero in the critical strip corresponds to a physical recognition event on the arithmetic ledger; the present result shows that any such zero produces a non-physical sensor, violating the thesis. It therefore feeds the derivation of the Riemann hypothesis from the RS thesis and closes the formalization gap between the concrete zeta function and the ledger framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.