canonicalThreshold_pos
plain-language theorem explainer
The canonical recognition threshold is strictly positive. Anyone needing a positive lower bound on that threshold constant in the RS forcing-chain scaffolding will cite this. The proof is a one-line unfold of the definition followed by linear arithmetic from the bound φ > 1.5.
Claim. The canonical threshold constant of the recognition lattice is strictly positive: $0 < \tau$, where $\tau$ is defined from the golden ratio $\varphi$ (so positivity follows once $\varphi > 3/2$).
background
This module is the first structural block of the RS forcing chain: every physical prediction is to derive from the cost $J(x)=\frac12(x+x^{-1})-1$, with zero sorry and zero axioms. The golden ratio $\varphi=(1+\sqrt5)/2$ is the self-similar fixed point forced later in the chain (T6).
The only upstream fact used here is the tighter lower bound $\varphi>1.5$, proved from $\sqrt5>2$. That bound is stronger than the elementary $\varphi>1$ and is exactly what linear arithmetic needs after the threshold definition is unfolded.
Sibling definitions in the same file introduce the domain cost and the canonical threshold itself; this lemma is the positivity certificate for that threshold constant.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then discharge the resulting inequality by linarith using the single lemma $\varphi>1.5$. No case splits, no induction, no further RS identities.
why it matters
Sits in Foundation RS Module 1, the structural layer that asserts the recognition lattice is axiom-free and sorry-free. Positivity of the canonical threshold is the elementary numeric gate before cost non-negativity and certificate inhabitation (domainCost_nonneg, RSForcingChain001Cert, cert_inhabited) can be trusted downstream.
No used_by edges are recorded yet, so the lemma is presently a local certificate rather than a cited step in T5–T8. It still anchors the numeric side of the forcing chain: once $\varphi$ is known to exceed $3/2$, every threshold built by subtracting a constant at most $1.5$ from $\varphi$ is automatically positive. That is the minimal arithmetic fact needed before J-cost comparisons and eight-tick bookkeeping begin.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.