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

ontological_exclusion

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)

 578theorem ontological_exclusion
 579    (bridge : EulerBoundaryBridgeAssumption) (sensor : DefectSensor) :
 580    EulerTraceAdmissible sensor → ¬ CostDivergent sensor := by

proof body

Term-mode proof.

 581  letI : PhysicallyRealizableLedger sensor := euler_physically_realizable sensor
 582  letI : DivergenceWitnessesBoundary sensor := euler_boundary_bridge bridge sensor
 583  exact ontological_exclusion_of_realizable sensor
 584
 585/-! ## §7. The unified RH theorem -/
 586
 587/-- **Unified RH**: no nonzero-charge sensor is compatible with the
 588Euler carrier under the ontological exclusion principle.
 589
 590Proof chain:
 5911. `euler_trace_admissible` — the carrier is admissible at every sensor (proved)
 5922. `euler_physically_realizable` — the Euler ledger is T1-bounded (proved)
 5933. `euler_boundary_bridge` — divergence would force boundary approach (bridge hypothesis)
 5944. `physicallyRealizableLedger_not_boundaryApproaching` — T1 forbids that (proved)
 5955. `nonzero_charge_cost_divergent` — nonzero charge IS cost-divergent (proved)
 5966. Contradiction: `sensor.charge ≠ 0 → False` -/

used by (2)

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

depends on (26)

Lean names referenced from this declaration's body.