`euler_physically_realizable`

definition

show as: view math explainer →

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

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Unification.UnifiedRH on GitHub at line 485.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 482  scalarDefectBounded := eulerScalarProxy_defect_bounded sensor
 483
 484/-- Explicit theorem form of the Euler realizability instance. -/
 485noncomputable def euler_physically_realizable (sensor : DefectSensor) :
 486    PhysicallyRealizableLedger sensor := by
 487  infer_instance
 488
 489/-- The Euler proxy is itself a realizable scalar path, so it cannot approach
 490the T1 boundary. This makes explicit why a separate bridge theorem is needed:
 491its bounded carrier scale does not collapse on its own. -/
 492theorem eulerScalarProxy_not_boundaryApproaching (sensor : DefectSensor) :
 493    letI : PhysicallyRealizableLedger sensor := euler_physically_realizable sensor
 494    ¬ BoundaryApproaching sensor := by
 495  intro hboundary
 496  letI : PhysicallyRealizableLedger sensor := euler_physically_realizable sensor
 497  exact physicallyRealizableLedger_not_boundaryApproaching sensor hboundary
 498
 499/-! ## §6. Boundary transport from divergence -/
 500
 501/-- A realizable ledger witnesses boundary transport if cost divergence would
 502force its scalar proxy state toward the T1 boundary.  This is the sharpened
 503replacement for the former ontological exclusion axiom. -/
 504class DivergenceWitnessesBoundary (sensor : DefectSensor)
 505    [PhysicallyRealizableLedger sensor] where
 506  toBoundary :
 507    EulerTraceAdmissible sensor → CostDivergent sensor → BoundaryApproaching sensor
 508
 509/-- If the concrete collapse scalar coming from the realized defect family
 510approaches `0`, then the Euler ledger scalar approaches the T1 boundary as
 511well.  After redefining the ledger scalar to be the realized collapse
 512observable in the nonzero-charge sector, this becomes a theorem. -/
 513class CollapseBoundaryTransport (sensor : DefectSensor)
 514    [PhysicallyRealizableLedger sensor] where
 515  toLedgerBoundary :

papers checked against this theorem

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