eulerScalarProxy_pos
plain-language theorem explainer
The Euler scalar proxy remains strictly positive for every defect sensor and every natural-number refinement depth. Researchers constructing T1-bounded realizability instances for the Euler carrier cite the result to guarantee the scalar state lies in the positive reals. The proof is a short tactic sequence that unfolds the proxy, invokes the already-proved positivity of the scalar gap, establishes nonnegativity of the normalized gap term, and closes with linarith.
Claim. For every defect sensor $s$ and every natural number $N$, the Euler scalar proxy satisfies $0 < p(s,N)$, where $p(s,N)$ denotes the scalar proxy state derived from the Euler carrier at sensor $s$ and refinement depth $N$.
background
The Unified RH module organizes T1-bounded realizability around three components: cost divergence for nonzero-charge sensors, Euler trace admissibility, and a physically realizable ledger whose scalar proxy state must remain positive and defect-bounded. The defect functional equals the J-cost on positive reals. The Euler scalar gap is the nonnegative quantity appearing in the denominator of the proxy; its positivity is established by a sibling lemma. Upstream results supply the reciprocal automorphism on the positive reals and the structure of J-cost on the phi-ladder.
proof idea
The proof unfolds the definition of the proxy. It applies the one_div_pos.mpr lemma, reducing the claim to positivity of the denominator. Nonnegativity of the gap follows from the already-proved eulerScalarGap_pos via le_of_lt. The normalized term gap/(N+1) is shown nonnegative by div_nonneg together with the positivity tactic. Linarith then yields the strict inequality.
why it matters
The theorem supplies the scalarStatePos field required by the eulerPhysicallyRealizableLedger instance, which in turn realizes the PhysicallyRealizableLedger structure for the Euler carrier. This step closes the chain from Euler trace admissibility to the T1-bounded ledger in the Unified RH architecture. It ensures the proxy cannot reach the T1 boundary x=0, consistent with the Recognition Science requirement that realizable ledgers remain uniformly bounded away from zero defect.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.