canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold used in this structural module is strictly positive. Anyone citing domain-cost or eight-tick threshold comparisons in the foundation layer needs this positivity fact. The proof is a one-line unfold-plus-linarith wrapper off the bound φ > 1.5.
Claim. The canonical threshold is strictly positive: $0 < T_{\mathrm{can}}$, where $T_{\mathrm{can}}$ is the module's canonical threshold (defined from the golden ratio $\varphi$).
background
Module RS_FDN_Structural_005 records structural facts for the Recognition Science eight-tick: one full traversal of the binary recognition lattice has period $2^D = 8$ (forcing landmark T7). Status is a pure structural theorem block (no sorry, no axioms).
The golden ratio $\varphi = (1+\sqrt{5})/2$ is the self-similar fixed point forced at T6. The upstream lemma used here tightens the elementary bound to $\varphi > 1.5$, via $\sqrt{5} > 2$. Sibling definitions in the module introduce a domain cost (nonnegative, with an evaluation identity) and the canonical threshold built from $\varphi$; positivity of that threshold is the present claim.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then discharge $0 < \cdots$ by linarith using the single fact $\varphi > 1.5$ (phi_gt_onePointFive). No further case splits or Recognition-Composition identities are required.
why it matters
Positivity of the canonical threshold is a tiny but necessary structural lemma in the eight-tick foundation pack: any later comparison that treats the threshold as a strict barrier (domain-cost lower bounds, recognition-lattice cutoffs) needs $T_{\mathrm{can}} > 0$ rather than a weak $\ge 0$. The module sits on the T7 eight-tick octave step of the forcing chain; $\varphi$ itself is the T6 fixed point. No downstream consumers are wired in the current graph, so this is presently a leaf certificate inside RSFDNStructural005Cert rather than a widely reused engine lemma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.