zeta_zero_gives_charged_sensor
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.
claimSuppose 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 in Recognition Science
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.
scope and limits
- Does not establish existence of any zeta zero.
- Does not compute multiplicity beyond the input assumption.
- Does not address zeros on the critical line Re=1/2.
- Does not derive the Riemann hypothesis.
formal statement (Lean)
20theorem zeta_zero_gives_charged_sensor
21 (ρ : ℂ) (_hzero : riemannZeta ρ = 0)
22 (hlo : 1 / 2 < ρ.re) (hhi : ρ.re < 1) :
23 ∃ sensor : DefectSensor, sensor.charge ≠ 0 ∧ sensor.realPart = ρ.re :=
proof body
Term-mode proof.
24 ⟨zetaDefectSensor ρ.re ⟨hlo, hhi⟩ 1,
25 zetaDefectSensor_charge_ne_zero ρ.re ⟨hlo, hhi⟩,
26 rfl⟩
27
28/-- Argument-principle data: a witnessed defect sensor carries genuine
29zeta-derived phase-family data. -/