canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold is a strictly positive real. Structural Standard-Model certificates in the eight-tick module cite it whenever a positive cutoff built from φ is required. The proof is a one-line wrapper: unfold the definition and finish by linear arithmetic from the bound φ > 1.5.
Claim. The canonical threshold (the real constant obtained by unfolding its definition in terms of the golden ratio $\varphi$) satisfies $0 < \tau_{\mathrm{can}}$.
background
This module records structural theorems for the Recognition Science Standard Model at the eight-tick scale: one full traversal of the binary recognition lattice has period $2^D = 8$ (T7), with status “structural theorem” (zero sorry, zero axiom).
The only external constant needed here is the golden ratio $\varphi = (1+\sqrt{5})/2$, forced earlier as the self-similar fixed point (T6). The upstream lemma phi_gt_onePointFive supplies the tight numerical bound $\varphi > 1.5$, proved from $\sqrt{5} > 2$. The canonical threshold is the local real constant defined from $\varphi$ (siblings also introduce a domain cost and its non-negativity).
proof idea
Pure wrapper. Unfold the definition of the canonical threshold, exposing an arithmetic expression in $\varphi$. Discharge the resulting strict inequality by linarith against the single fact $\varphi > 1.5$ from phi_gt_onePointFive. No further lemmas or case splits.
why it matters
Positivity of the canonical threshold is the elementary gate that lets later structural certificates treat the cutoff as a genuine positive scale rather than a formal symbol. It sits inside RS_STD_Structural_005 alongside domain-cost non-negativity and the inhabited certificate RSSTDStructural005Cert, all supporting the eight-tick octave (T7) and the $D=3$ forcing (T8). No downstream consumers are recorded yet; the lemma is infrastructure for any argument that needs a strictly positive φ-derived threshold inside the Standard-Model structural layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.