pith. machine review for the scientific record. sign in
theorem proved tactic proof

concreteEulerLedgerOntologyInterface_exists

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)

 181theorem concreteEulerLedgerOntologyInterface_exists (sensor : DefectSensor) :
 182    ∃ pkg : EulerLedgerOntologyInterface sensor,
 183      (∀ support : PrimeSupport,
 184        LedgerForcing.balanced (pkg.directedLedger.stage support)) ∧
 185      (∀ support : PrimeSupport, ∀ agent : ℕ,
 186        LedgerForcing.net_flow (pkg.directedLedger.stage support) agent = 0) ∧
 187      (∃ carrier : RegularCarrier,
 188        carrier.radius = sensor.realPart - 1 / 2 ∧ 0 < carrier.radius) ∧
 189      (letI : PhysicallyRealizableLedger sensor := pkg.realizableProxy

proof body

Tactic-mode proof.

 190       ∃ K : ℝ, ∀ N : ℕ,
 191        IndisputableMonolith.Foundation.LawOfExistence.defect
 192          (PhysicallyRealizableLedger.scalarState (sensor := sensor) N) ≤ K) := by
 193  refine ⟨concreteEulerLedgerOntologyInterface sensor, ?_, ?_, ?_, ?_⟩
 194  · intro support
 195    exact (concreteEulerLedgerOntologyInterface sensor).directedLedger.stage_balanced support
 196  · intro support agent
 197    exact (concreteEulerLedgerOntologyInterface sensor).directedLedger.stage_net_flow_zero support agent
 198  · exact (concreteEulerLedgerOntologyInterface sensor).has_regular_carrier
 199  · exact (concreteEulerLedgerOntologyInterface sensor).scalarDefectBounded
 200
 201end NumberTheory
 202end IndisputableMonolith

depends on (14)

Lean names referenced from this declaration's body.