canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold appearing in the RS gravity structural layer is strictly positive. Gravity and certificate authors cite it whenever a positivity gate is needed on that threshold. The argument is a one-line unfold-plus-linarith wrapper off the bound φ > 1.5.
Claim. The canonical threshold built from the golden ratio $\varphi$ is strictly positive: $0 < \tau_{\mathrm{can}}$.
background
This lives in the first RS gravity structural module, whose stated setting is the forced triple $J(x)=\tfrac12(x+1/x)-1$, $\varphi$ the golden ratio, and $D=3$, with zero sorry and zero axioms. The cost $J$ is the unique nonnegative generator of the Recognition Composition Law (T5); $\varphi$ is the self-similar fixed point forced at T6.
The only upstream fact used is the tighter numerical bound $\varphi>1.5$, obtained from $\sqrt5>2$ so that $(1+\sqrt5)/2>3/2$. The canonical threshold is the local constant obtained by unfolding a definition that is linear in $\varphi$ against that bound; positivity is then immediate arithmetic.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then invoke linarith on the single lemma $\varphi>1.5$. No case split, no induction, no further RS structure.
why it matters
Supplies the positivity gate for the structural gravity certificate package in this module (the inhabited RSGRVStructural001Cert / cert siblings). It is a tiny but mandatory arithmetic step once $\varphi$ is fixed at T6: any threshold written as a positive multiple or shift of $\varphi-3/2$ inherits strict positivity from $\varphi>1.5$. Downstream use count is currently zero outside the module, so the lemma is infrastructure for the local certificate rather than a cross-module workhorse. It does not itself force $D=3$ or the eight-tick octave; those sit elsewhere in the T0–T8 chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.