HonestPhaseChargeZeroBridge
plain-language theorem explainer
HonestPhaseChargeZeroBridge asserts that every ZetaPhaseFamilyData carries zero sensor charge. Analysts on the pure analytic route to the Riemann hypothesis cite it to discharge the charge-zero requirement inside ZeroFreeCriterion without needing a total-cost bound. The declaration is a bare structure definition whose single field directly encodes the needed universal statement.
Claim. A structure $B$ such that for every zeta phase family datum $zfd$, the charge of $zfd$.sensor equals zero.
background
The AnalyticTrace module assembles an axiom-free interface for the pure analytic route to RH. Its target is the ZeroFreeCriterion structure, which packages three requirements: log-derivative bounds on the critical strip, nonvanishing of the carrier function, and an honest phase-family map that converts any nonzero-charge sensor into a ZetaPhaseFamilyData object. The HonestPhaseChargeZeroBridge supplies precisely the charge-zero conclusion that the honest_phase_family field of ZeroFreeCriterion demands.
proof idea
This is a structure definition containing a single field. No lemmas or tactics are invoked; the field is the direct statement that charge vanishes for every honest phase datum.
why it matters
The structure feeds direct_rh_from_honestPhaseChargeZeroBridge, which composes it with zeroFreeCriterion_of_honestPhaseChargeZeroBridge to obtain the analytic RH core. It also participates in the equivalence honestPhaseAdmissibilityBridge_iff_chargeZeroBridge, linking the charge-zero route to the admissibility route. Within the Recognition framework it closes one slot of the pure analytic path, complementing the ontology route that relies on EulerBoundaryBridgeAssumption.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.