HonestPhaseCostBridge_of_rh
plain-language theorem explainer
If every witnessed defect sensor carries zero charge, then the honest phase cost bridge holds, so every honest sampled family has bounded annular cost. Number theorists formalizing the Riemann hypothesis through sampled Euler traces would cite this result to close the analytic route. The proof extracts zero charge via sensor and family mappings, then invokes realized defect cost boundedness together with honest-phase excess boundedness.
Claim. Assume that every witnessed defect sensor $s$ satisfies charge$(s)=0$. Then for every such $s$ and every zeta phase family datum $z$ with matching sensor, the realized defect annular cost of the sampled family obtained from $z$ is bounded.
background
The Analytic Trace module assembles an axiom-free RH bridge from carrier-side infrastructure. HonestPhaseCostBridge is the structure whose sole field requires that every honest sampled family (obtained from a zeta phase family datum) has bounded realized defect annular cost; once this holds, the general defect-cost theorem forces zero charge. The module eliminates prior axioms by deriving zero winding from holomorphy and nonvanishing, and by proving floor coverage if and only if charge equals zero. Upstream results supply the cost function as the J-cost of a recognition event and the multiplicative recognizer cost on positive ratios.
proof idea
The tactic proof introduces the sensor and zeta phase family datum together with the sensor-matching hypothesis. It extracts the zero-charge fact for the original sensor from the global hypothesis, transports it first to the defect sensor via simpa on the matching, then to the sampled family via simpa on the toSampledFamily and family_sensor projections. The proof concludes by exact application of realizedDefectCostBounded_of_charge_zero_and_excessBounded, supplying the transported zero charge and the honestPhaseFamily_excess_bounded lemma.
why it matters
This theorem supplies the zero-charge-implies-bridge direction of the equivalence HonestPhaseCostBridge_iff_rh, which states that the bounded-cost bridge is logically identical to RH for witnessed sensors. It is invoked by honestPhaseCostBridge_of_EBBA to show that the ontology route via EulerBoundaryBridgeAssumption immediately closes the analytic route as well. The result therefore completes the pure-analytic path to the zero-free criterion inside the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.