eulerCarrierRadius_pos

formal source

 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:
 142
 143`gap(sensor) = M_C(σ₀) * (σ₀ - 1/2) / C(σ₀)`,
 144
 145where `σ₀ = sensor.realPart`, `M_C = carrierDerivBound`, and `C = carrierValue`.
 146
 147This packages three concrete Euler ingredients into one dimensionless scalar:
 148the carrier log-derivative bound, the admissible strip radius, and the carrier
 149amplitude itself. -/
 150noncomputable def eulerScalarGap (sensor : DefectSensor) : ℝ :=
 151  carrierDerivBound sensor.realPart * eulerCarrierRadius sensor /
 152    carrierValue sensor.realPart
 153
 154/-- The normalized Euler stiffness parameter is strictly positive. -/
 155theorem eulerScalarGap_pos (sensor : DefectSensor) :
 156    0 < eulerScalarGap sensor := by
 157  unfold eulerScalarGap
 158  exact div_pos
 159    (mul_pos
 160      (carrierDerivBound_pos sensor.in_strip.1)
 161      (eulerCarrierRadius_pos sensor))
 162    (carrier_pos sensor.in_strip.1)
 163
 164/-- Concrete sensor-indexed scalarization extracted from Euler/carrier data.
 165
 166At refinement depth `N`, we attenuate the normalized carrier stiffness by the