pith. machine review for the scientific record. sign in
theorem proved term proof

rh_chain_summary_legacy

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 371theorem rh_chain_summary_legacy :
 372    (∀ (sensor : DefectSensor) (hm : sensor.charge ≠ 0),
 373      DeprecatedDefectAnnularCostBounded sensor hm) →
 374    ∀ (sensor : DefectSensor), sensor.charge ≠ 0 → False :=

proof body

Term-mode proof.

 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. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (25)

Lean names referenced from this declaration's body.