`concreteEulerLedgerOntologyInterface`

definition

show as: view math explainer →

module: IndisputableMonolith.NumberTheory.DirectedEulerLedger
domain: NumberTheory
line: 145 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.NumberTheory.DirectedEulerLedger on GitHub at line 145.

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

 142
 143/-- Every sensor has the combined directed-ledger / admissibility /
 144realizability package. -/
 145noncomputable def concreteEulerLedgerOntologyInterface (sensor : DefectSensor) :
 146    EulerLedgerOntologyInterface sensor where
 147  directedLedger := concreteDirectedEulerLedgerSystem sensor
 148  admissibleTrace := euler_trace_admissible sensor
 149  realizableProxy := euler_physically_realizable sensor
 150
 151/-- The ontology package carries a compatible regular Euler carrier. -/
 152theorem EulerLedgerOntologyInterface.has_regular_carrier
 153    {sensor : DefectSensor} (pkg : EulerLedgerOntologyInterface sensor) :
 154    ∃ carrier : RegularCarrier,
 155      carrier.radius = sensor.realPart - 1 / 2 ∧ 0 < carrier.radius :=
 156  pkg.admissibleTrace.carrier_compatible
 157
 158/-- The realizability proxy in the ontology package is positive at every depth. -/
 159theorem EulerLedgerOntologyInterface.scalarState_pos
 160    {sensor : DefectSensor} (pkg : EulerLedgerOntologyInterface sensor) (N : ℕ) :
 161    letI : PhysicallyRealizableLedger sensor := pkg.realizableProxy
 162    0 < PhysicallyRealizableLedger.scalarState (sensor := sensor) N := by
 163  letI : PhysicallyRealizableLedger sensor := pkg.realizableProxy
 164  simpa using PhysicallyRealizableLedger.scalarStatePos (sensor := sensor) N
 165
 166/-- The realizability proxy in the ontology package has uniformly bounded T1
 167defect. -/
 168theorem EulerLedgerOntologyInterface.scalarDefectBounded
 169    {sensor : DefectSensor} (pkg : EulerLedgerOntologyInterface sensor) :
 170    letI : PhysicallyRealizableLedger sensor := pkg.realizableProxy
 171    ∃ K : ℝ, ∀ N : ℕ,
 172      IndisputableMonolith.Foundation.LawOfExistence.defect
 173        (PhysicallyRealizableLedger.scalarState (sensor := sensor) N) ≤ K := by
 174  letI : PhysicallyRealizableLedger sensor := pkg.realizableProxy
 175  simpa using PhysicallyRealizableLedger.scalarDefectBounded (sensor := sensor)

papers checked against this theorem

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