honestPhaseCostBridge_of_EBBA
plain-language theorem explainer
Assuming the Euler boundary bridge assumption, the honest phase cost bridge holds for witnessed defect sensors. This supplies the bounded annular cost property needed for honest zeta phase families in the analytic trace. Researchers closing the ontology route to the Riemann hypothesis cite it to show that the boundary assumption suffices for all active analytic routes. The proof is a term-mode application of the RH-implies-cost-bridge theorem, constructing the zero-charge hypothesis by contradiction via the unified RH result.
Claim. If the Euler boundary bridge assumption holds, then the honest phase cost bridge holds: for every witnessed defect sensor $s$ and zeta phase family data $z$ with $z$.sensor matching $s$.toDefectSensor, the realized defect annular cost of the corresponding sampled family is bounded.
background
In the Analytic Trace module the honest phase cost bridge is the structure whose sole field requires that every honest sampled zeta phase family has bounded realized defect annular cost. This bound, once available, lets the general defect-cost theorem force zero charge on witnessed sensors. The module builds axiom-free infrastructure for the Riemann hypothesis, with the ontology route depending on the external EulerBoundaryBridgeAssumption from UnifiedRH. Upstream, HonestPhaseCostBridge_of_rh states that if every witnessed sensor has charge zero then the cost bridge follows, since zero-charge families carry zero topological floor.
proof idea
The proof is a one-line term wrapper invoking HonestPhaseCostBridge_of_rh. The required hypothesis (every witnessed defect sensor has charge zero) is supplied by a lambda that proceeds by contradiction: assume nonzero charge for a sensor, then apply unified_rh to the given bridge and the sensor (after simpa on the assumption) to obtain the needed contradiction.
why it matters
This result shows that the EulerBoundaryBridgeAssumption immediately yields the honest phase cost bridge, which is then fed into zeroFreeCriterion_of_EBBA to close the ontology route to the zero-free criterion. The module doc notes that this proves closing EBBA closes all active routes simultaneously. Within the Recognition framework it links the ontology bridge to the cost-boundedness step required for charge-zero conclusions in the analytic trace, advancing the pure analytic target while still relying on the external assumption.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.