ArgumentPrincipleSensorCert
The ArgumentPrincipleSensorCert structure records that any witnessed defect sensor with nonzero charge is accompanied by genuine zeta phase-family data derived from the argument principle, and that every zero of the Riemann zeta function inside the critical strip produces a charged defect sensor. Researchers assembling the RH-from-RCL thesis would cite this certificate to link analytic zeros to physical defect data. The declaration is a bare structure definition whose fields are instantiated downstream by honest_argument_principle_phase_family.
claimA certificate consists of two assertions: for every witnessed defect sensor with nonzero charge there exists zeta phase family data such that the underlying sensor equals the defect sensor and the phase family is attached to the same sensor; and for every complex zero $ρ$ of the Riemann zeta function satisfying $1/2 < ρ.re < 1$ there exists a defect sensor with nonzero charge whose real part equals $ρ.re$.
background
In the NumberTheory module the argument-principle sensor bridge isolates the analytic fact required by the RH-from-RCL route: zeros of the zeta function produce annular winding charge. The module packages the phase-lift stack already proved in ArgumentPrincipleProved so that it can be consumed directly by the final RH assembly. A DefectSensor records the multiplicity (charge) and real part of a zero of ζ(s), viewed as a pole of ζ⁻¹. A WitnessedDefectSensor strengthens this by retaining the full center ρ together with an explicit meromorphic-order witness that the charge originates from zetaReciprocal itself. ZetaPhaseFamilyData packages the phase samples obtained from the Weierstrass factorization of zetaReciprocal near such a zero, together with the matching sensor and order data.
proof idea
The declaration is a structure definition that simply declares two fields. No tactics or lemmas are applied inside the structure itself; the concrete values for the fields are supplied later by the definition argumentPrincipleSensorCert, which sets witnessed_phase_family to the function honest_argument_principle_phase_family and zero_gives_charged_sensor to zeta_zero_gives_charged_sensor.
why it matters in Recognition Science
This certificate supplies the zeroDefect component required by both RSPhysicalThesisDataLogic and RSPhysicalThesisData, the decomposed data structures that underpin the Recognition Science physical thesis. It thereby closes the analytic half of the RH-from-RCL route by guaranteeing that zeta zeros inside the strip carry nonzero charge and genuine phase-family data. The module doc-comment states that the repository already contains the phase-lift stack; the present structure merely exposes it as an explicit certificate for the final assembly.
scope and limits
- Does not prove the existence of any zeta zero.
- Does not locate zeros on the critical line.
- Does not compute explicit phase values or winding numbers.
- Does not address the functional equation or other global properties of zeta.
- Does not connect the charge to the Recognition Science phi-ladder or mass formula.
formal statement (Lean)
30structure ArgumentPrincipleSensorCert where
31 witnessed_phase_family :
32 ∀ sensor : WitnessedDefectSensor, sensor.charge ≠ 0 →
33 ∃ zfd : ZetaPhaseFamilyData,
34 zfd.sensor = sensor.toDefectSensor ∧
35 zfd.phaseFamily.sensor = sensor.toDefectSensor
36 zero_gives_charged_sensor :
37 ∀ ρ : ℂ, riemannZeta ρ = 0 → 1 / 2 < ρ.re → ρ.re < 1 →
38 ∃ sensor : DefectSensor, sensor.charge ≠ 0 ∧ sensor.realPart = ρ.re
39
40/-- The current argument-principle sensor certificate. -/