def
definition
EulerBoundaryBridgeAssumption
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Unification.UnifiedRH on GitHub at line 535.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
bridge -
defect -
is -
as -
is -
for -
is -
is -
divergence -
and -
DefectSensor -
that -
CollapseBoundaryTransport -
euler_physically_realizable -
PhysicallyRealizableLedger
used by
-
direct_rh_from_EBBA_via_analytic -
direct_rh_from_zero_free_criterion -
honestPhaseCostBridge_of_EBBA -
rh_chain_summary_legacy -
zeroFreeCriterion_of_EBBA -
honest_argument_principle_phase_family -
BoundaryTransportCert -
boundaryTransportCert_iff_EBBA -
cascade_doubly_exponential_lower -
cost_finiteness_iff_rh -
cost_finiteness_of_EBBA -
EBBA_iff_rh -
EBBA_of_cost_finiteness -
EBBA_of_rh -
euler_boundary_bridge -
euler_divergence_witnesses_boundary -
ontological_exclusion -
single_scalar_obstruction -
unified_rh -
UnifiedRHCert -
unified_rh_cert_of_bridge
formal source
532/-- Remaining ontology bridge after separating the bounded Euler realizability
533proxy from the realized collapse observable: collapse of the realized defect
534family must transport to boundary approach for the actual realizability proxy. -/
535def EulerBoundaryBridgeAssumption : Prop :=
536 ∀ sensor : DefectSensor,
537 letI : PhysicallyRealizableLedger sensor := euler_physically_realizable sensor
538 CollapseBoundaryTransport sensor
539
540/-- The old boundary-bridge interface is now recovered as a theorem: divergence
541gives a concrete realized-defect collapse scalar that approaches `0`, and the
542remaining proxy-transport hypothesis converts that collapse into boundary
543approach for the bounded Euler realizability proxy. -/
544theorem euler_divergence_witnesses_boundary
545 (bridge : EulerBoundaryBridgeAssumption) (sensor : DefectSensor) :
546 DivergenceWitnessesBoundary sensor := by
547 letI : PhysicallyRealizableLedger sensor := euler_physically_realizable sensor
548 letI : CollapseBoundaryTransport sensor := bridge sensor
549 refine ⟨?_⟩
550 intro _ hdiv
551 have hm : sensor.charge ≠ 0 := costDivergent_charge_ne_zero sensor hdiv
552 exact CollapseBoundaryTransport.toLedgerBoundary (sensor := sensor) hm
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)