HonestPhaseCostBridge_iff_rh

formal source

 409framework. The proof uses `not_realizedDefectAnnularCostBounded` (which
 410shows bounded cost is impossible for nonzero charge) for the forward
 411direction, and zero-charge bounded-cost for the backward direction. -/
 412theorem HonestPhaseCostBridge_iff_rh :
 413    HonestPhaseCostBridge ↔
 414      (∀ sensor : WitnessedDefectSensor, sensor.charge = 0) :=
 415  ⟨fun hb sensor => by
 416    by_contra hm
 417    exact direct_rh_from_honestPhaseCostBridge hb sensor hm,
 418   HonestPhaseCostBridge_of_rh⟩
 419
 420/-! ### §8. Cross-route connection: ontology → analytic -/
 421
 422/-- The ontology bridge immediately supplies the honest-phase cost bridge.
 423This proves closing EBBA closes ALL active routes simultaneously. -/
 424theorem honestPhaseCostBridge_of_EBBA
 425    (bridge : Unification.UnifiedRH.EulerBoundaryBridgeAssumption) :
 426    HonestPhaseCostBridge :=
 427  HonestPhaseCostBridge_of_rh (fun sensor => by
 428    by_contra hm
 429    exact Unification.UnifiedRH.unified_rh bridge sensor.toDefectSensor (by simpa using hm))
 430
 431/-- The ontology bridge also supplies a complete `ZeroFreeCriterion`. -/
 432noncomputable def zeroFreeCriterion_of_EBBA
 433    (bridge : Unification.UnifiedRH.EulerBoundaryBridgeAssumption) :
 434    ZeroFreeCriterion :=
 435  zeroFreeCriterion_of_honestPhaseCostBridge (honestPhaseCostBridge_of_EBBA bridge)
 436
 437/-- Direct witnessed-sensor RH from the ontology bridge through the analytic route. -/
 438theorem direct_rh_from_EBBA_via_analytic
 439    (bridge : Unification.UnifiedRH.EulerBoundaryBridgeAssumption) :
 440    ∀ (sensor : WitnessedDefectSensor), sensor.charge ≠ 0 → False :=
 441  rh_from_zero_free_criterion (zeroFreeCriterion_of_EBBA bridge)
 442