canonicalThreshold_pos
plain-language theorem explainer
The canonical recognition threshold is strictly positive. Anyone working the discrete RS energy spectrum or the first excited (recognition-quantum) level needs this sign. The proof is a one-line unfold of the threshold definition followed by linear arithmetic from the bound φ > 1.5.
Claim. The canonical threshold is positive: $0 < \varphi - 1.5$ (equivalently $0 < J(\varphi)$), where $\varphi$ is the golden ratio and $J$ is the unique RS cost.
background
The module builds the Recognition Spectrum of $H_{RS}$ on the $\varphi$-ladder: energies $E_n = J(\varphi^n),\hbar_R,\omega_0$ for $n=0,1,2,\ldots$. The ground state is $E_0=0$; the first excited level $E_1=J(\varphi),\hbar_R,\omega_0$ is the recognition quantum. Status is structural (zero sorry, zero axiom).
$J$ is the unique cost forced by T5, $J(x)=(x+x^{-1})/2-1$. For the golden ratio $\varphi=(1+\sqrt{5})/2$ one has the exact identity $J(\varphi)=\varphi-3/2$. The sibling definition canonicalThreshold is therefore this first-rung cost (equivalently $\varphi-1.5$).
The sole upstream fact is the tighter lower bound $\varphi>1.5$, obtained from $\sqrt{5}>2$.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold (exposing an expression equivalent to $\varphi-1.5$), then discharge $0<\varphi-1.5$ by linarith using the lemma $\varphi>1.5$.
why it matters
Positivity of the first rung is the minimal sign fact needed before any certificate that the RS spectrum is nonnegative with a strictly positive recognition quantum. It sits inside the structural package that also defines domain cost, the spectrum certificate, and its inhabitation. In the forcing chain it rests on T5 ($J$-uniqueness) and T6 ($\varphi$ as self-similar fixed point): once $J(\varphi)=\varphi-3/2$ is identified, the elementary bound $\varphi>1.5$ closes the inequality. No downstream edges are recorded yet; the immediate consumers are the sibling spectrum certificate constructions in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.