`eulerPhysicallyRealizableLedger`

definition

show as: view math explainer →

module: IndisputableMonolith.Unification.UnifiedRH
domain: Unification
line: 477 · 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 477.

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

formal source

 474/-- The Euler carrier is physically realizable in the T1-bounded sense with
 475realizability scalar given by the bounded carrier-derived proxy
 476`eulerScalarProxy`. -/
 477noncomputable instance eulerPhysicallyRealizableLedger (sensor : DefectSensor) :
 478    PhysicallyRealizableLedger sensor where
 479  admissible := euler_trace_admissible sensor
 480  scalarState := eulerScalarProxy sensor
 481  scalarStatePos := eulerScalarProxy_pos sensor
 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

papers checked against this theorem

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