argumentPrincipleSensorCert
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not establish the existence of any zeta zeros.
- Does not prove the Riemann hypothesis.
- Does not supply the boundary transport certificate required for the full physical thesis data.
- Does not address the multiplicity or location of zeros beyond the critical strip condition.
Lean usage
example (b : BoundaryTransportCert) : RSPhysicalThesisData := rsPhysicalThesisData_of_boundaryTransport bformal statement (Lean)
41def argumentPrincipleSensorCert : ArgumentPrincipleSensorCert where
42 witnessed_phase_family := fun sensor hm =>
proof body
Definition body.
43 honest_argument_principle_phase_family sensor hm
44 zero_gives_charged_sensor := zeta_zero_gives_charged_sensor
45
46end NumberTheory
47end IndisputableMonolith