canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold built from the golden-ratio fixed point φ is strictly positive. Anyone using the structural cost or domain-cost cutoffs in the RS mathematics layer can cite this as the positivity certificate. The proof is a one-line wrapper: unfold the definition and finish by linear arithmetic from the bound φ > 1.5.
Claim. The canonical threshold $\tau$ (the RS cutoff constructed from the self-similar fixed point $\varphi$) satisfies $0 < \tau$.
background
This module records structural facts about the RS self-similar fixed point $\varphi = 1 + 1/(1+1/(1+\cdots))$, the unique positive solution of $\varphi = 1 + 1/\varphi$ (equivalently $\varphi^2 = \varphi + 1$). Status is a pure structural theorem: zero sorry, zero axioms.
The sibling definition canonicalThreshold is the cutoff constant used with the local domain cost; in RS units it is the positive quantity built from $\varphi$ (the same scale as the Berry creation threshold $\varphi^{-1} = \varphi - 1$). Positivity of that cutoff is the elementary gate before any comparison of costs against the threshold.
The sole upstream fact is the tighter lower bound $\varphi > 1.5$, obtained from $\sqrt{5} > 2$ via the closed form $\varphi = (1+\sqrt{5})/2$. That bound is more than enough to force any linear expression of the form $\varphi - 1$ (or $\varphi - 3/2$) to be positive.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then apply linarith to the hypothesis $\varphi > 1.5$ from phi_gt_onePointFive. No further lemmas or case splits are required: after unfolding, the goal is a linear inequality in $\varphi$ that follows immediately from the numerical lower bound.
why it matters
Structural Module 6 packages the elementary positivity facts that sit under RS $\varphi$-uniqueness (forcing-chain landmark T6: $\varphi$ forced as the self-similar fixed point). A positive canonical threshold is the gate that lets domain-cost comparisons and threshold tests be well-posed on the $\varphi$-ladder.
No downstream consumers are wired in the graph yet (used_by is empty), so this lemma is presently a leaf certificate inside the module's own cert bundle (RSMTHStructural006Cert / cert_inhabited). It closes the positivity side of the structural package rather than feeding a named parent theorem. It does not itself prove uniqueness of $\varphi$; it only guarantees the cutoff built from $\varphi$ is strictly above zero.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.