`euler_boundary_bridge`

definition

show as: view math explainer →

module: IndisputableMonolith.Unification.UnifiedRH
domain: Unification
line: 556 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Unification.UnifiedRH on GitHub at line 556.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

 553    (realizedDefectCollapseBoundaryApproaching_of_nonzero_charge sensor hm)
 554
 555/-- Explicit theorem form of the proved boundary bridge. -/
 556def euler_boundary_bridge
 557    (bridge : EulerBoundaryBridgeAssumption) (sensor : DefectSensor) :
 558    DivergenceWitnessesBoundary sensor :=
 559  euler_divergence_witnesses_boundary bridge sensor
 560
 561/-! ## §6. The ontological exclusion theorem -/
 562
 563/-- Generic ontological exclusion theorem: any physically realizable ledger
 564equipped with a divergence-to-boundary bridge cannot be cost-divergent. -/
 565theorem ontological_exclusion_of_realizable (sensor : DefectSensor)
 566    [PhysicallyRealizableLedger sensor] [DivergenceWitnessesBoundary sensor] :
 567    EulerTraceAdmissible sensor → ¬ CostDivergent sensor := by
 568  intro hadm hdiv
 569  have hboundary : BoundaryApproaching sensor :=
 570    DivergenceWitnessesBoundary.toBoundary (sensor := sensor) hadm hdiv
 571  exact physicallyRealizableLedger_not_boundaryApproaching sensor hboundary
 572
 573/-- **Ontological Exclusion Principle.**
 574
 575For the Euler carrier, admissibility plus the boundary-transport bridge imply
 576that cost divergence is impossible.  This theorem replaces the old axiom of
 577the same name. -/
 578theorem ontological_exclusion
 579    (bridge : EulerBoundaryBridgeAssumption) (sensor : DefectSensor) :
 580    EulerTraceAdmissible sensor → ¬ CostDivergent sensor := by
 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

papers checked against this theorem

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