zetaDefectSensor_charge_one
plain-language theorem explainer
The declaration shows that a DefectSensor built from a hypothetical zeta zero in the open strip with multiplicity one carries charge exactly one. Researchers formalizing the Riemann hypothesis inside Recognition Science cite this when constructing explicit sensors before invoking the ontological dichotomy. The proof is a direct simplification that unfolds the constructor of zetaDefectSensor.
Claim. Let $σ ∈ ℝ$ satisfy $½ < σ < 1$. The defect sensor constructed from the Riemann zeta function at real part $σ$ with multiplicity 1 has charge equal to 1.
background
The Zeta–Ledger Bridge module connects Mathlib’s riemannZeta to the abstract DefectSensor and PhysicallyExists framework proved in UnifiedRH. A DefectSensor records an integer charge (multiplicity) together with a realPart lying in the open strip (½,1). The upstream definition zetaDefectSensor takes realPart, a strip witness, and multiplicity, then builds the sensor by setting charge := multiplicity, realPart := realPart, and in_strip := h_strip.
proof idea
The proof is a one-line wrapper that applies the definition of zetaDefectSensor. Simplification unfolds the constructor record and matches the supplied multiplicity argument 1 directly to the charge field.
why it matters
This result supplies the base case for the family of charge lemmas that feed RSPhysicalThesis and the derivation of Mathlib’s RiemannHypothesis from the RS thesis, as described in the module documentation. It closes the concrete-to-abstract gap between a strip zero of ζ and a nonzero-charge sensor whose physical existence is denied by the ontological dichotomy. The declaration touches the open question whether any such strip zeros can exist under the RS framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.