eulerScalarGap_pos
plain-language theorem explainer
The declaration proves that the normalized Euler stiffness parameter is strictly positive for every defect sensor. Researchers modeling T1-bounded realizability in the Unified RH architecture cite it to guarantee that the scalar proxy state derived from Euler carrier data stays positive at all refinement depths. The proof is a term-mode reduction that unfolds the gap definition and invokes positivity of multiplication and division on the carrier derivative bound, admissible radius, and carrier value.
Claim. For every defect sensor $s$, the normalized Euler stiffness parameter satisfies $0 < $ normalized Euler stiffness parameter$(s)$.
background
The Unified RH module organizes T1-bounded realizability around four components: Cost Divergent (annular cost grows unbounded for nonzero charge), Euler Trace Admissible (Euler carrier convergent with bounded log derivative), Physically Realizable Ledger (sensor-indexed scalar proxy with bounded T1 defect), and Divergence Witnesses Boundary (external bridge hypothesis). The normalized Euler stiffness parameter appears in the refinement construction $x_N = 1 / (1 + $ gap$/(N+1))$, where gap is extracted from carrier derivative bound, strip radius, and carrier value. Upstream results include carrier_pos from engineering modules establishing $0 < 5phi$ and the structure of nuclear densities in phi-tiers from NucleosynthesisTiers.
proof idea
The proof unfolds eulerScalarGap and applies div_pos to the product of carrierDerivBound_pos (sensor.in_strip.1) and eulerCarrierRadius_pos sensor, divided by carrier_pos (sensor.in_strip.1). It is a one-line term proof that chains the three positivity lemmas directly.
why it matters
This theorem feeds eulerScalarProxy_pos and eulerScalarProxy_defect_bounded, which together show the Euler scalar proxy stays positive with uniformly bounded T1 defect. It supplies the Euler carrier instance for the Physically Realizable Ledger component, advancing the module's proof chain toward T1 forbidding boundary approach. In the Recognition Science framework it supports the Euler instantiation within the T1-bounded architecture, consistent with the phi-ladder and eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.