direct_rh_from_honestPhaseChargeZeroBridge
plain-language theorem explainer
An honest-phase charge-zero bridge forces every witnessed defect sensor to have zero charge. Researchers working the pure analytic route to the Riemann hypothesis cite this result to close the zero-free criterion without external axioms. The proof is a one-line term wrapper that feeds the bridge into the zero-free criterion theorem after constructing the criterion instance.
Claim. If honest zeta phase family data yields sensor charge zero, then every witnessed defect sensor has charge zero (equivalently, charge nonzero leads to contradiction).
background
The Analytic Trace module supplies an axiom-free analytic route to the Riemann hypothesis by assembling sampled Euler carriers, contour winding, and phase data. HonestPhaseChargeZeroBridge is the structure asserting that for every zeta phase family datum the associated sensor charge equals zero; this directly discharges the charge-zero field of the ZeroFreeCriterion. The module replaces two former axioms with proved statements: zero winding from holomorphy plus nonvanishing, and floor coverage if and only if charge zero. Upstream results include the zero-free criterion theorem and the bridge-to-criterion construction used in the proof.
proof idea
Term-mode one-line wrapper. It applies rh_from_zero_free_criterion to the ZeroFreeCriterion produced by zeroFreeCriterion_of_honestPhaseChargeZeroBridge on the supplied bridge.
why it matters
The declaration supplies the final link for the pure analytic RH route inside the module, showing that any honest-phase charge-zero bridge is sufficient to reach the zero-free criterion. It complements the ontology route that relies on EulerBoundaryBridgeAssumption and targets the analytic route described in the module documentation. The result sits at the end of the carrier-side infrastructure that eliminates prior axioms while preserving the direct path from phase data to charge zero.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.