theorem
proved
euler_trace_admissible
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Unification.UnifiedRH on GitHub at line 111.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
of -
of -
defect -
forces -
cost -
cost -
of -
from -
of -
of -
DefectSensor -
carrierDerivBound_pos -
carrier_nonvanishing -
sensor_carrier_compatible -
EulerTraceAdmissible
used by
formal source
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
131sensor location to the critical line `Re(s) = 1/2`. -/
132noncomputable def eulerCarrierRadius (sensor : DefectSensor) : ℝ :=
133 sensor.realPart - 1 / 2
134
135/-- The carrier-compatible radius is positive in the strip. -/
136theorem eulerCarrierRadius_pos (sensor : DefectSensor) :
137 0 < eulerCarrierRadius sensor := by
138 unfold eulerCarrierRadius
139 linarith [sensor.in_strip.1]
140
141/-- A normalized Euler stiffness parameter extracted from genuine carrier data: