canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold built from the golden ratio is strictly positive. Module-8 certificate authors and anyone comparing domain costs against that scale would cite it. Proof is a one-line unfold of the threshold definition plus linear arithmetic from the bound φ > 1.5.
Claim. The canonical threshold $T$ constructed from the golden ratio $\varphi=(1+\sqrt{5})/2$ satisfies $0 < T$.
background
Foundation Module 8 is the structural block for RS φ-uniqueness: $\varphi=(1+\sqrt{5})/2$ is the unique fixed point of recognition recursion (forcing-chain landmark T6). Status is fully proved (no sorry, no axioms).
The only upstream fact used here is the elementary bound $\varphi>1.5$, obtained from $\sqrt{5}>2$. After unfolding, the canonical threshold is a real expression in $\varphi$ whose positivity is then a linear consequence of that bound. Sibling definitions in the module introduce a domain cost and the threshold itself as the comparison scale against which cost nonnegativity is organized.
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 RS identities are required.
why it matters
Supplies the positivity half of the Module-8 threshold apparatus that sits beside domain-cost nonnegativity and the module certificate (RSForcingChain008Cert / cert_inhabited). In the broader forcing chain this is bookkeeping under T6 (φ forced as the self-similar fixed point), not a new forcing step. No recorded downstream consumers yet; the lemma exists so later cost comparisons and the structural cert can quote a named positivity fact rather than re-running arithmetic on φ.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.