 613* `boundary_bridge` — an external bridge transports collapse to ledger boundary
 614* `divergence` — nonzero charge forces cost divergence
 615* `rh` — no nonzero-charge sensor exists -/
 616structure UnifiedRHCert where
 617  t1_barrier :
 618    ∀ C : ℝ, ∃ ε > 0, ∀ x : ℝ, 0 < x → x < ε →
 619      C < IndisputableMonolith.Foundation.LawOfExistence.defect x
 620  admissibility : ∀ (sensor : DefectSensor), EulerTraceAdmissible sensor
 621  realizability : ∀ (sensor : DefectSensor), PhysicallyRealizableLedger sensor
 622  realized_collapse :
 623    ∀ (sensor : DefectSensor) (hm : sensor.charge ≠ 0),
 624      RealizedCollapseBoundaryApproaching sensor hm
 625  t1_no_boundary_crossing :
 626    ∀ (sensor : DefectSensor),
 627      letI : PhysicallyRealizableLedger sensor := realizability sensor
 628      ¬ BoundaryApproaching sensor
 629  boundary_bridge : EulerBoundaryBridgeAssumption
 630  divergence : ∀ (sensor : DefectSensor), sensor.charge ≠ 0 → CostDivergent sensor
 631  rh : ∀ (sensor : DefectSensor), sensor.charge ≠ 0 → False
 632
 633/-- Any supplied Euler bridge hypothesis yields the corresponding unified RH
 634certificate. -/
 635noncomputable def unified_rh_cert_of_bridge
 636    (bridge : EulerBoundaryBridgeAssumption) : UnifiedRHCert where
 637  t1_barrier := t1_cost_barrier
 638  admissibility := euler_trace_admissible
 639  realizability := euler_physically_realizable
 640  realized_collapse := realizedDefectCollapseBoundaryApproaching_of_nonzero_charge
 641  t1_no_boundary_crossing := by
 642    intro sensor
 643    letI : PhysicallyRealizableLedger sensor := euler_physically_realizable sensor
 644    exact physicallyRealizableLedger_not_boundaryApproaching sensor
 645  boundary_bridge := bridge
 646  divergence := nonzero_charge_cost_divergent

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.