`EulerLedgerOntologyInterface`

definition

show as: view math explainer →

module: IndisputableMonolith.NumberTheory.DirectedEulerLedger
domain: NumberTheory
line: 135 · 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 135.

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

 132
 133/-- The finite-to-directed arithmetic package, connected to the ontology-side
 134admissibility and realizability interfaces. -/
 135structure EulerLedgerOntologyInterface (sensor : DefectSensor) where
 136  /-- Concrete finite stages over prime supports. -/
 137  directedLedger : DirectedEulerLedgerSystem sensor
 138  /-- Analytic admissibility of the associated Euler trace. -/
 139  admissibleTrace : EulerTraceAdmissible sensor
 140  /-- T1-bounded realizability proxy coming from the Euler carrier. -/
 141  realizableProxy : PhysicallyRealizableLedger sensor
 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

papers checked against this theorem

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