eulerCarrierRadius_pos
The theorem shows that the Euler carrier radius is strictly positive whenever a defect sensor lies inside the admissible strip. Workers on the Unified RH architecture cite it to confirm positivity of derived stiffness scalars before invoking the physically realizable ledger. The proof is a one-line wrapper that unfolds the radius definition and applies linear arithmetic to the first component of the sensor's strip membership hypothesis.
claimLet $r_E$ denote the Euler carrier radius extracted from the carrier log-derivative bound, admissible strip radius, and carrier amplitude. For any defect sensor $s$ satisfying the strip condition, $r_E(s) > 0$.
background
The Unified RH module organizes T1-bounded realizability into cost divergence, Euler trace admissibility, and physically realizable ledgers. The Euler carrier radius packages the carrier log-derivative bound, the admissible strip radius, and the carrier amplitude into a single positive scalar. Upstream results supply the neighborhood radius definition from cellular automata and the carrier frequency $5phi$ from engineering modules, together with the arithmetic extraction and integration-gap constants used to build the sensor type.
proof idea
The proof unfolds the definition of the Euler carrier radius, exposing an expression whose positivity follows directly from the first conjunct of the sensor's in_strip hypothesis. The linarith tactic then closes the inequality without further lemmas.
why it matters in Recognition Science
The result is invoked by the downstream theorem establishing strict positivity of the normalized Euler stiffness parameter. It closes the Euler Trace Admissibility component of the T1-bounded realizability architecture, confirming that the carrier remains inside the positive region required for the physically realizable ledger. The step aligns with the eight-tick octave and phi-ladder structure of the forcing chain.
scope and limits
- Does not prove existence of any defect sensor.
- Does not address annular cost divergence.
- Does not establish convergence of the full Euler trace.
- Does not quantify the radius beyond the strip.
formal statement (Lean)
136theorem eulerCarrierRadius_pos (sensor : DefectSensor) :
137 0 < eulerCarrierRadius sensor := by
proof body
Term-mode proof.
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. -/