pith. machine review for the scientific record. sign in
def definition def or abbrev

concreteEulerLedgerOntologyInterface

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 145noncomputable def concreteEulerLedgerOntologyInterface (sensor : DefectSensor) :
 146    EulerLedgerOntologyInterface sensor where
 147  directedLedger := concreteDirectedEulerLedgerSystem sensor

proof body

Definition body.

 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)
 176
 177/-- Concrete theorem form: every sensor has a directed arithmetic Euler ledger,
 178an admissible Euler trace, and a T1-bounded realizability proxy. This is the
 179current strongest proved bridge from arithmetic Euler data into the ontology
 180layer. -/

used by (4)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (8)

Lean names referenced from this declaration's body.