charge_zero_of_honest_phase_of_costBridge
plain-language theorem explainer
An honest-phase cost bridge together with a witnessed defect sensor and matching zeta phase family data forces the sensor charge to zero. Analytic number theorists following the pure analytic route to the Riemann hypothesis in Recognition Science cite this to discharge the final charge-zero obligation. The proof unpacks the existential witness, pulls the bounded annular cost from the bridge, invokes the honest-phase charge-zero lemma on the sampled family, and simplifies the sensor identifications.
Claim. Let $hb$ be an honest-phase cost bridge, let $sensor$ be a witnessed defect sensor, and suppose there exists zeta phase family data $zfd$ such that $zfd.sensor = sensor.toDefectSensor$ and $zfd.phaseFamily.sensor = sensor.toDefectSensor$. Then the charge of $sensor$ is zero.
background
The Analytic Trace module assembles an axiom-free interface for the Riemann hypothesis by replacing former axioms on contour winding and the argument principle with proved statements such as eulerSampledFloorCovered_iff_charge_zero. In this setting the HonestPhaseCostBridge is the structure whose sole field supplies, for any witnessed defect sensor and zeta phase family data with matching sensors, a proof that the realized defect annular cost of the sampled family is bounded. This bounded-cost datum is the last missing input to the general defect-cost theorem that forces charge zero. Upstream results calibrate the underlying J-cost via the eight-tick phase definition and the cost functions induced by multiplicative recognizers and observer forcing events.
proof idea
The tactic proof performs rcases on the existential hypothesis for the zeta phase family data. It applies the cost_bounded_of_honest_phase field of the bridge to obtain RealizedDefectAnnularCostBounded for the sampled family. It then calls honestPhaseFamily_charge_zero_of_costBounded on the family data and the bounded-cost witness to conclude that the underlying sensor charge is zero, followed by two simpa steps that transport the equality across the sensor identifications.
why it matters
This theorem supplies the charge-zero step required by zeroFreeCriterion_of_honestPhaseCostBridge, which constructs a complete ZeroFreeCriterion from any honest-phase cost bridge. It therefore closes the pure analytic route to the Riemann hypothesis independently of Vector C and of the ontology route that relies on EulerBoundaryBridgeAssumption. Within the Recognition Science framework it completes the elimination of the former axioms listed in the module documentation and aligns with the eight-tick octave and J-cost calibration that underwrite the annular bounds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.