`eulerLedgerScalarState_pos`

proved

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Unification.UnifiedRH on GitHub at line 467.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 464  simp [eulerLedgerScalarState, hm]
 465
 466/-- The Euler ledger scalar is always positive. -/
 467theorem eulerLedgerScalarState_pos (sensor : DefectSensor) (N : ℕ) :
 468    0 < eulerLedgerScalarState sensor N := by
 469  by_cases hzero : sensor.charge = 0
 470  · simp [eulerLedgerScalarState, hzero]
 471  · simpa [eulerLedgerScalarState, hzero] using
 472      realizedDefectCollapseScalar_pos sensor hzero N
 473
 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

papers checked against this theorem

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