canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold built from the golden ratio is strictly positive. Anyone working the structural rung-spacing package needs this to keep cutoffs and domain costs on the right side of zero. Proof is a one-line unfold plus linear arithmetic from the bound φ > 1.5.
Claim. The canonical threshold associated to $\varphi$-rung spacing is strictly positive: $0 < \tau$, where $\tau$ is defined from the golden ratio $\varphi = (1+\sqrt{5})/2$.
background
Module 8 of the Foundation structural series fixes RS rung spacing: adjacent rungs differ by the factor $\varphi \approx 1.618$. The local package defines a canonical threshold from $\varphi$ and pairs it with a domain cost; both sit in a zero-sorry structural certificate.
The only upstream fact used here is the tighter lower bound $\varphi > 1.5$, obtained from $\sqrt{5} > 2$ so that $(1+\sqrt{5})/2 > 3/2$. That bound is more than enough to force any linear expression of the form $\varphi - c$ with $c \le 1.5$ (in particular the usual $\varphi-1 = \varphi^{-1}$ gap) to be positive.
In the broader RS ladder, rung steps and mass yardsticks are powers of $\varphi$; positivity of the structural threshold keeps those cutoffs non-vacuous.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then discharge $0 < \tau$ by linarith using the lemma $\varphi > 1.5$. No case split and no further RS lemmas.
why it matters
Closes the positivity obligation for the module-8 structural certificate (siblings include the domain cost non-negativity and the inhabited cert). Downstream use count is presently zero, so this is a leaf fact inside the certificate rather than a widely cited lemma.
In the forcing chain it sits under T6: $\varphi$ is the self-similar fixed point that sets rung spacing. The mass formula on the $\varphi$-ladder and the Berry threshold $\varphi^{-1}$ both presuppose that the structural gap is positive; this theorem records that elementary fact inside Lean with no axioms or sorries.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.