eulerCarrierRadius_pos
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.