canonicalThreshold_pos
plain-language theorem explainer
The canonical recognition threshold is a strictly positive real. Cite it whenever a gap-45 or domain-cost comparison needs a positive cutoff built from φ. The proof is a one-line unfold-plus-linarith wrapper off the bound φ > 1.5.
Claim. The canonical recognition threshold is strictly positive: $0 < T_{\mathrm{can}}$, where $T_{\mathrm{can}}$ is the real constant obtained by unfolding the module's canonical-threshold definition (a simple expression in the golden ratio $\varphi$).
background
Module 3 of the RS forcing-chain foundation records the structural gap identity $g_D = D^2(D+2)$. At the forced spatial dimension $D = 3$ this is $g_3 = 45$, the minimum depth for self-reference. The module is marked structural: zero sorry, zero axioms.
The golden ratio $\varphi = (1+\sqrt{5})/2$ is the self-similar fixed point forced at T6. The upstream lemma phi_gt_onePointFive supplies the tighter numerical bound $\varphi > 1.5$, proved from $\sqrt{5} > 2$. The canonical threshold is a real constant defined from $\varphi$ in this module (sibling of the domain-cost family); positivity is the elementary gate before any comparison against domain cost.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then invoke linarith with the single fact $\varphi > 1.5$. No case split and no further RS lemmas are required; linear arithmetic closes the inequality once the definition is expanded.
why it matters
Sits in the structural layer of Foundation Module 3 (gap-45 at $D=3$). It underwrites any later argument that treats the canonical threshold as a positive cutoff when comparing domain costs or when anchoring the minimum self-reference depth. The forcing-chain landmarks T6 ($\varphi$ forced) and T8 ($D=3$) are the ambient reasons the constant is well-defined and relevant. The local used-by list is empty, so the lemma is presently a leaf certificate rather than an intermediate step in a larger proved chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.