def definition def or abbrev

`euler_boundary_bridge`

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

formal statement (Lean)

 556def euler_boundary_bridge
 557    (bridge : EulerBoundaryBridgeAssumption) (sensor : DefectSensor) :
 558    DivergenceWitnessesBoundary sensor :=

proof body

Definition body.

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

used by (3)

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

divergence_witnesses_boundary_of_cert in IndisputableMonolith.NumberTheory.BoundaryTransport decl_use
no_cost_divergent_sensor_of_boundary_transport in IndisputableMonolith.NumberTheory.BoundaryTransport decl_use
ontological_exclusion in IndisputableMonolith.Unification.UnifiedRH decl_use

depends on (8)

Lean names referenced from this declaration's body.

bridge in IndisputableMonolith.ClassicalBridge.Fluids.CPM2D decl_use
cost in IndisputableMonolith.Foundation.MultiplicativeRecognizerL4 decl_use
cost in IndisputableMonolith.Foundation.ObserverForcing decl_use
divergence in IndisputableMonolith.NavierStokes.DiscreteNSOperator decl_use
DefectSensor in IndisputableMonolith.NumberTheory.CostCoveringBridge decl_use
DivergenceWitnessesBoundary in IndisputableMonolith.Unification.UnifiedRH decl_use
EulerBoundaryBridgeAssumption in IndisputableMonolith.Unification.UnifiedRH decl_use
euler_divergence_witnesses_boundary in IndisputableMonolith.Unification.UnifiedRH decl_use