canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold constant of this cosmology module is strictly positive. Cosmology certificates and domain-cost arguments cite it to keep cutoffs well-defined and above zero. Proof is a one-line wrapper: unfold the definition, then linear arithmetic from φ > 1.5.
Claim. The canonical threshold (the module's fixed cutoff built from the golden ratio $\varphi$) satisfies $0 < \mathrm{threshold}$.
background
Module RS_COS_Structural_005 is a structural cosmology layer for Recognition Science: the eight-tick octave (period $2^D = 8$) as one full traversal of the binary recognition lattice. Status is structural (0 sorry, 0 axiom).
The golden ratio $\varphi = (1+\sqrt{5})/2$ is the self-similar fixed point of the forcing chain (T6). Upstream lemma phi_gt_onePointFive gives the tight real bound $\varphi > 1.5$, proved from $\sqrt{5} > 2$. The canonical threshold is a real constant defined from $\varphi$ in this file; sibling facts also record nonnegativity of the associated domain cost (J-cost style recognition cost on the lattice).
Positivity of the threshold is the elementary gate before the structural certificate RSCOSStructural005Cert can be inhabited.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold so the goal is an explicit real inequality in $\varphi$. Discharge with linarith using the upstream lemma that $\varphi > 1.5$. No case split and no further Recognition lemmas.
why it matters
Keeps the cosmology structural stack honest: a named positive cutoff rather than an implicit nonzero assumption. Sits beside domainCost_nonneg and feeds the module certificate (RSCOSStructural005Cert / cert_inhabited), which packages the eight-tick structural claims. Ties to framework landmark T7 (eight-tick octave, period $2^3$) and the $\varphi$-native constants used throughout RS cosmology. No downstream edges are recorded yet; the lemma is local hygiene for the cert.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.