charge_zero_of_honest_phase_of_chargeZeroBridge
plain-language theorem explainer
Given a direct honest-phase charge-zero bridge and a witnessed defect sensor equipped with matching zeta phase family data, the sensor charge is zero. Researchers pursuing the pure analytic route to the Riemann hypothesis cite this to discharge the charge-zero requirement inside the zero-free criterion. The proof is a short tactic sequence that extracts the phase family datum, applies the bridge statement, and substitutes the sensor equality via simplification.
Claim. Let $hb$ be a structure asserting that every zeta phase family datum has sensor charge zero. Let $sensor$ be a witnessed defect sensor. Suppose there exists zeta phase family datum $zfd$ such that $zfd$ matches $sensor$ on both its sensor and phase-family sensor components. Then the charge of $sensor$ is zero.
background
The AnalyticTrace module assembles an axiom-free RH bridge from analytic trace infrastructure. Former axioms (zero-winding and argument-principle charge zero) have been replaced by proved statements such as contour winding from holomorphy and floor-coverage iff charge zero. Two routes remain: the ontology route via external EulerBoundaryBridgeAssumption and the pure analytic route that targets a ZeroFreeCriterion built from honest zeta inverse phase data.
proof idea
The proof performs case analysis on the existence hypothesis to obtain the zeta phase family datum and the sensor equality. It applies the bridge's universal charge-zero statement to that datum. Two simplification steps then transfer the zero charge first to the defect sensor's to-defect-sensor component and finally to the original sensor.
why it matters
This discharges the charge-zero obligation required by the honest_phase_family field of ZeroFreeCriterion. It is invoked inside the construction zeroFreeCriterion_of_honestPhaseChargeZeroBridge that assembles the full criterion for the pure analytic route. The module positions this as the direct analytic path to RH, complementary to the ontology route in UnifiedRH.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.