canonicalThreshold_pos
plain-language theorem explainer
The canonical recognition threshold (an RS constant built from the golden ratio) is strictly positive. Cite this wherever a positive threshold is needed before domain-cost comparisons in the eight-tick foundation layer. Proof is a one-line unfold plus linear arithmetic from φ > 1.5.
Claim. The canonical threshold is strictly positive: $0 < T_{\mathrm{can}}$, where $T_{\mathrm{can}}$ is the RS canonical threshold defined from the golden ratio $\varphi=(1+\sqrt{5})/2$.
background
Foundation Module 2 records the RS eight-tick cycle: period $2^D=2^3=8$ states per recognition epoch, forced by spatial dimension $D=3$. The module is marked structural (zero sorry, zero axioms).
The golden ratio $\varphi$ is the self-similar fixed point forced at T6 of the unified forcing chain. A tight elementary lower bound is available upstream: $\varphi>1.5$, proved from $\sqrt{5}>2$ so that $(1+\sqrt{5})/2>3/2$.
The canonical threshold is the named constant in this module obtained by unfolding a short expression in $\varphi$. Its positivity is the elementary sign fact needed before nonnegativity and comparison results on domain cost.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then discharge the resulting real inequality by linear arithmetic, feeding in the upstream lemma $\varphi>1.5$. No case split or nonlinear estimate is required.
why it matters
Lives in the T7 eight-tick structural layer of the forcing chain (period $2^3=8$, forced by $D=3$). Sibling results in the same module treat domain cost and its nonnegativity; a strictly positive threshold is the arithmetic prerequisite those comparisons rely on.
No recorded downstream consumers yet. The lemma closes a local obligation so later forcing-chain certificates (and the module certificate itself) can assume a positive threshold without re-deriving the bound on $\varphi$. It does not touch mass-ladder rungs, $\alpha$, or the J-cost uniqueness step (T5).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.