rh_chain_summary_legacy

formal source

 368
 369/-- ⚠ DEPRECATED: routes through the inconsistent `defect_annular_cost_bounded`.
 370Use `unified_rh` (ontology) or `direct_rh_from_honestPhaseCostBridge` (analytic). -/
 371theorem rh_chain_summary_legacy :
 372    (∀ (sensor : DefectSensor) (hm : sensor.charge ≠ 0),
 373      DeprecatedDefectAnnularCostBounded sensor hm) →
 374    ∀ (sensor : DefectSensor), sensor.charge ≠ 0 → False :=
 375  fun hbounded sensor hm => analytic_rh sensor hm (hbounded sensor hm)
 376
 377/-! ### §7. Cross-route connection and RH-equivalence
 378
 379The ontology route (`EulerBoundaryBridgeAssumption`) and the analytic route
 380(`HonestPhaseCostBridge`) are both RH-equivalent. The ontology route is
 381strictly stronger: it works for all `DefectSensor`s (abstract), while the
 382analytic route covers `WitnessedDefectSensor`s (actual zeros of ζ).
 383
 384Closing EBBA immediately supplies HonestPhaseCostBridge, ZeroFreeCriterion,
 385and all downstream analytic certificates. -/
 386
 387/-- RH (for witnessed sensors) implies `HonestPhaseCostBridge`. If every
 388witnessed sensor has charge 0, then every honest sampled family has
 389bounded cost because zero-charge families have zero topological floor. -/
 390theorem HonestPhaseCostBridge_of_rh
 391    (hrh : ∀ sensor : WitnessedDefectSensor, sensor.charge = 0) :
 392    HonestPhaseCostBridge where
 393  cost_bounded_of_honest_phase := by
 394    intro sensor zfd hzsensor
 395    have hcharge_sensor : sensor.charge = 0 := hrh sensor
 396    have hcharge_ds : zfd.sensor.charge = 0 := by
 397      simpa [hzsensor] using hcharge_sensor
 398    have hcharge_fam : (zfd.phaseFamily.toSampledFamily).sensor.charge = 0 := by
 399      simpa [DefectPhaseFamily.toSampledFamily, zfd.family_sensor] using hcharge_ds
 400    exact realizedDefectCostBounded_of_charge_zero_and_excessBounded
 401      (zfd.phaseFamily.toSampledFamily) hcharge_fam