EulerTraceAdmissible

formal source

  97
  98These three properties are proved for ALL sensors from the Euler product
  99convergence data. -/
 100structure EulerTraceAdmissible (sensor : DefectSensor) : Prop where
 101  carrier_compatible : ∃ (carrier : RegularCarrier),
 102    carrier.radius = sensor.realPart - 1/2 ∧ 0 < carrier.radius
 103  carrier_nonvanishing : ∀ σ, 1/2 < σ → carrierValue σ ≠ 0
 104  carrier_deriv_bounded : ∀ σ, 1/2 < σ → 0 < carrierDerivBound σ
 105
 106/-- Every `DefectSensor` has an admissible Euler trace.
 107
 108This follows directly from the Euler instantiation certificate:
 109`sensor_carrier_compatible`, `carrier_nonvanishing`, and
 110`carrierDerivBound_pos`. -/
 111theorem euler_trace_admissible (sensor : DefectSensor) :
 112    EulerTraceAdmissible sensor where
 113  carrier_compatible := sensor_carrier_compatible sensor
 114  carrier_nonvanishing := fun _ hσ => carrier_nonvanishing hσ
 115  carrier_deriv_bounded := fun _ hσ => carrierDerivBound_pos hσ
 116
 117/-! ## §3. T1 cost barrier (re-export) -/
 118
 119/-- The T1 scalar cost barrier from the Law of Existence:
 120approaching the non-existence boundary forces arbitrarily large defect cost.
 121
 122`∀ C, ∃ ε > 0, ∀ x ∈ (0,ε), defect(x) > C` -/
 123theorem t1_cost_barrier (C : ℝ) :
 124    ∃ ε > 0, ∀ x : ℝ, 0 < x → x < ε →
 125      C < IndisputableMonolith.Foundation.LawOfExistence.defect x :=
 126  IndisputableMonolith.Foundation.LawOfExistence.nothing_cannot_exist C
 127
 128/-! ## §4. Physically realizable ledgers -/
 129
 130/-- The carrier-compatible radius attached to a sensor: the distance from the