pith. machine review for the scientific record. sign in
structure definition def or abbrev

UnifiedRHCert

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)

 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

proof body

Definition body.

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

used by (1)

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

depends on (11)

Lean names referenced from this declaration's body.