argumentPrincipleSensorCert
plain-language theorem explainer
This definition assembles the argument-principle sensor certificate by wiring the honest phase-family construction directly to the zeta-zero sensor map. Researchers following the RH-from-RCL derivation cite it as the zeroDefect datum inside the physical thesis decomposition. The construction is a direct record literal that delegates both fields to already-proved upstream theorems.
Claim. The argument-principle sensor certificate is the structure consisting of a witnessed phase family map (sending each nonzero-charge witnessed defect sensor to zeta-derived phase family data) together with a map (sending each zeta zero with real part strictly between 1/2 and 1 to a nonzero-charge defect sensor).
background
The module isolates the analytic fact needed by the RH-from-RCL route: zeros give annular winding charge. The repository already has the phase-lift stack in ArgumentPrincipleProved; here we package that stack as the explicit certificate consumed by the final RH assembly. ArgumentPrincipleSensorCert is the structure requiring a witnessed_phase_family that, for any WitnessedDefectSensor with nonzero charge, produces ZetaPhaseFamilyData whose sensor matches, and a zero_gives_charged_sensor that, for any zeta zero in the open critical strip, produces a DefectSensor with nonzero charge and matching real part.
proof idea
This is a definition that constructs the certificate record by setting witnessed_phase_family to the theorem honest_argument_principle_phase_family and zero_gives_charged_sensor to the theorem zeta_zero_gives_charged_sensor.
why it matters
This declaration supplies the zeroDefect field in rsPhysicalThesisData_of_boundaryTransport and is referenced inside logicData_of_boundaryTransport. It completes the packaging of the analytic certificate required for the boundary-transport route to the physical thesis. The module doc states it isolates the analytic fact needed by the RH-from-RCL route.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.