eulerScalarProxy_pos
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not establish boundedness of the T1 defect itself.
- Does not address whether the annular cost diverges.
- Does not prove the full PhysicallyRealizableLedger instance.
- Does not depend on specific numerical values of the sensor or N beyond the stated types.
Lean usage
scalarStatePos := eulerScalarProxy_pos sensorformal statement (Lean)
177theorem eulerScalarProxy_pos (sensor : DefectSensor) (N : ℕ) :
178 0 < eulerScalarProxy sensor N := by
proof body
Tactic-mode proof.
179 unfold eulerScalarProxy
180 apply one_div_pos.mpr
181 have hgap_nonneg : 0 ≤ eulerScalarGap sensor := le_of_lt (eulerScalarGap_pos sensor)
182 have hfrac_nonneg : 0 ≤ eulerScalarGap sensor / (N + 1 : ℝ) := by
183 exact div_nonneg hgap_nonneg (by positivity)
184 linarith
185
186/-- Closed form of the T1 defect on the reciprocal-affine Euler scalar proxy. -/