ArgumentPrincipleSensorCert
plain-language theorem explainer
ArgumentPrincipleSensorCert packages two statements that link nonzero-charge witnessed defect sensors to genuine zeta-derived phase families and that map critical-strip zeta zeros to charged defect sensors. Researchers assembling the RH-from-RCL decomposition cite the structure as the explicit analytic certificate consumed by RSPhysicalThesisDataLogic. The structure is introduced directly as a record whose fields are populated by the sibling definitions honest_argument_principle_phase_family and zeta_zero_gives_charged_sensor.
Claim. A structure whose first field asserts that every witnessed defect sensor with nonzero charge admits a zeta phase family data record whose underlying defect sensor and phase-family sensor both equal the original sensor; whose second field asserts that every zero of the Riemann zeta function with real part strictly between 1/2 and 1 yields a defect sensor of nonzero charge whose real-part coordinate equals that zero's real part.
background
DefectSensor records only the integer charge (multiplicity of the zero of zeta) and the real part of its location inside the critical strip. WitnessedDefectSensor strengthens this by adding the full complex center rho together with an explicit meromorphic-order witness that the charge arises from zetaReciprocal at that point. ZetaPhaseFamilyData further augments the sensor with a QuantitativeLocalFactorization witness and the associated DefectPhaseFamily whose phase samples are taken from the Weierstrass factorization of zetaReciprocal itself.
proof idea
The declaration is a bare structure definition; its two fields are named but receive no proof body inside the structure. The concrete inhabitants are supplied later by the sibling definition argumentPrincipleSensorCert, which simply applies honest_argument_principle_phase_family to the first field and zeta_zero_gives_charged_sensor to the second.
why it matters
The structure supplies the zeroDefect component required by both RSPhysicalThesisData and RSPhysicalThesisDataLogic, thereby closing the analytic half of the RH-from-RCL route. It isolates the fact that zeros produce annular winding charge, exactly the datum demanded by the module's stated purpose of packaging the phase-lift stack for final assembly. No open scaffolding remains inside the structure itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.