canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold, a local RS constant built from the golden ratio φ, is strictly positive. Module-7 certificate authors and anyone comparing domain costs against that threshold cite this sign fact. The proof is a one-line wrapper: unfold the definition and close by linear arithmetic from the bound φ > 1.5.
Claim. The canonical threshold $\tau$ (the Module-7 constant built from the golden ratio $\varphi$) satisfies $0 < \tau$.
background
Foundation Module 7 records the RS count law: at spatial dimension $D=3$, there are exactly $2^D-1=7$ independent observable categories. Status is structural (zero sorry, zero axiom). The golden ratio $\varphi=(1+\sqrt{5})/2$ is the self-similar fixed point forced at T6 of the unified forcing chain.
The sole upstream input is the tighter lower bound $\varphi>1.5$, obtained from $\sqrt{5}>2$. The canonical threshold is the sibling constant in this module against which domain-cost comparisons are made; its positivity is the elementary sign fact needed before those comparisons can be stated.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then discharge the resulting inequality by linarith using the lemma $\varphi>1.5$. No further case splits or Recognition-Composition identities are required.
why it matters
Supplies the sign of the Module-7 threshold so the local forcing certificate (RSForcingChain007Cert and its inhabited cert) can treat threshold comparisons as well-formed. Sits inside the structural count-law package $2^D-1=7$ at $D=3$ (T8), with $\varphi$ coming from T6. No external used-by edges are recorded yet; the lemma is infrastructure for the module cert rather than a cross-module export. It does not itself prove the count law or force $D=3$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.