zeta_zero_gives_charged_sensor
plain-language theorem explainer
A zero of the Riemann zeta function with real part strictly between 1/2 and 1 produces a defect sensor whose charge is nonzero and equals the multiplicity. Researchers deriving the Riemann hypothesis from the recognition composition law cite this bridge. The proof is a direct term that instantiates the sensor from the real part and applies the pre-proved charge nonzeroness property.
Claim. Suppose the Riemann zeta function satisfies $zeta(rho)=0$ for $rho in mathbb{C}$ with $frac{1}{2} < operatorname{Re}(rho) < 1$. Then there exists a defect sensor whose charge is nonzero and whose real part equals $operatorname{Re}(rho)$.
background
The module isolates the analytic fact that zeros of zeta supply annular winding charge for the argument principle. A DefectSensor records the multiplicity (charge) of a zero, its real part, and the strip condition. The auxiliary construction zetaDefectSensor takes the real part, the strip bounds, and multiplicity to build the sensor. Upstream results supply the eight-tick phases from EightTick.phase and the defect functional from LawOfExistence.defect, which equals J for positive arguments and underpins the phase-lift stack.
proof idea
The proof is a one-line term that applies zetaDefectSensor to the real part of rho together with the strip hypotheses and multiplicity one, then pairs the result with zetaDefectSensor_charge_ne_zero and reflexivity for the real-part equality.
why it matters
This theorem supplies the zero-to-charged-sensor direction required by argumentPrincipleSensorCert, which packages the phase-family data for the final RH assembly. It closes the ontological dichotomy for hypothetical zeros in the right half-strip, consistent with the eight-tick phase structure and the defect functional. The result is fully proved with no remaining scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.