argumentPrincipleSensorCert
plain-language theorem explainer
The argument principle sensor certificate bundles the proved honest phase family data for nonzero-charge defect sensors with the mapping from Riemann zeta zeros in the critical strip to charged sensors. It is cited by the RH-from-RCL assembly when constructing physical thesis data from boundary transport. The definition is a direct one-line wrapper that instantiates the certificate structure using the upstream honest_argument_principle_phase_family theorem and the zeta_zero_gives_charged_sensor result.
Claim. The argument-principle sensor certificate consists of a function that, for every witnessed defect sensor with nonzero charge, yields zeta-derived phase family data satisfying the sensor equality, together with a function that maps every zero $ρ$ of the Riemann zeta function with $1/2 < Re(ρ) < 1$ to a defect sensor with nonzero charge equal to the real part of $ρ$.
background
In the Argument-Principle Sensor Bridge module the analytic fact required by the RH-from-RCL route is isolated: zeros of zeta produce annular winding charge. The structure ArgumentPrincipleSensorCert packages witnessed phase family data and the zero-to-sensor map. The witnessed_phase_family field requires that for a WitnessedDefectSensor with nonzero charge there exists ZetaPhaseFamilyData whose sensor matches the defect sensor. The zero_gives_charged_sensor field asserts that a zero in the open critical strip yields a DefectSensor with nonzero charge. This relies on the honest_argument_principle_phase_family theorem, which states that if zeta has a zero of multiplicity m at rho with Re(rho)>1/2 the Euler factorization yields a DefectPhaseFamily with charge m, and on zeta_zero_gives_charged_sensor which produces the sensor via zetaDefectSensor.
proof idea
This definition constructs the certificate by setting the witnessed_phase_family field to the result of honest_argument_principle_phase_family applied to the sensor and the charge inequality, and the zero_gives_charged_sensor field directly to the zeta_zero_gives_charged_sensor theorem. It is a one-line wrapper that applies the upstream proved results without additional reasoning.
why it matters
This certificate supplies the zeroDefect component in rsPhysicalThesisData_of_boundaryTransport, completing the explicit data bundle for the physical thesis except for the boundary transport bridge. It is used in logicData_of_boundaryTransport to build the logic-aware decomposition. In the Recognition Science framework it closes the analytic input to the RH-from-RCL route by confirming that zeros in the critical strip generate nonzero charge sensors, consistent with the ontological dichotomy and the argument principle applied to zetaReciprocal.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.