IndisputableMonolith.NumberTheory.ArgumentPrincipleSensor
ArgumentPrincipleSensor shows that any zero of zeta with real part exceeding 1/2 produces a nonphysical nonzero-charge sensor via the ontological dichotomy. Researchers formalizing the Recognition Science version of the Riemann Hypothesis cite this module. It composes the already-proved argument-principle elimination with the zeta-ledger bridge to witness the sensor implication.
claimIf $s$ satisfies $s = 1/2 + it$ with $t$ real and $s$ is a zero of the Riemann zeta function, then the associated defect sensor is nonphysical and carries nonzero charge, by the ontological dichotomy.
background
The module imports ArgumentPrincipleProved, which eliminates argument_principle_sampling as an axiom and upgrades the analytic route toward witnessed ζ^{-1} phase-family data, and ZetaLedgerBridge, which closes the formalization gap between the abstract DefectSensor / PhysicallyExists framework (proved in UnifiedRH.lean) and Mathlib's concrete riemannZeta. The supplied doc-comment states the core implication: a zero of zeta in the right half of the critical strip gives a nonphysical nonzero-charge sensor by the already-proved ontological dichotomy. Sibling declarations include zeta_zero_gives_charged_sensor and the certification objects ArgumentPrincipleSensorCert and argumentPrincipleSensorCert.
proof idea
This module assembles the two imported results to derive the charged-sensor implication; the structure is a direct composition of the proved argument-principle sampling elimination with the zeta-ledger bridge, without new analytic lemmas.
why it matters in Recognition Science
The module feeds RSPhysicalThesisDecomposition, which replaces the opaque RSPhysicalThesis dependency with a structured bundle of the exact ingredients needed for the RH proof. It supplies the explicit nonphysical consequence of a right-half-plane zero, closing one link in the Recognition Science chain from the argument principle to physical existence.
scope and limits
- Does not locate or count any zeta zeros.
- Does not prove the Riemann Hypothesis.
- Does not supply numerical checks of the sensor.
- Does not treat zeros in the left half-plane.