`eulerCarrierRadius`

definition

show as: view math explainer →

module: IndisputableMonolith.Unification.UnifiedRH
domain: Unification
line: 132 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Unification.UnifiedRH on GitHub at line 132.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 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:
 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)

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.