eulerScalarGap

formal source

 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
 167scale `1/(N+1)` and then convert it to a positive scalar state
 168
 169`x_N = 1 / (1 + gap/(N+1))`.
 170
 171This is no longer a placeholder constant: it is computed from the actual Euler
 172carrier value, derivative bound, and admissible strip radius of the sensor. -/
 173noncomputable def eulerScalarProxy (sensor : DefectSensor) (N : ℕ) : ℝ :=
 174  1 / (1 + eulerScalarGap sensor / (N + 1 : ℝ))
 175
 176/-- The concrete Euler scalar proxy stays positive at every refinement depth. -/
 177theorem eulerScalarProxy_pos (sensor : DefectSensor) (N : ℕ) :
 178    0 < eulerScalarProxy sensor N := by
 179  unfold eulerScalarProxy
 180  apply one_div_pos.mpr