canonicalThreshold_pos
plain-language theorem explainer
The canonical recognition threshold for an RS qubit channel is strictly positive. Anyone using the φ^{-1} overhead factor in qubit capacity bounds needs this fact. The proof unfolds the threshold to an expression in φ and closes positivity by linear arithmetic from φ > 1.5.
Claim. The canonical threshold is positive: $0 < T_{\mathrm{can}}$. Under the module convention $T_{\mathrm{can}} = \varphi - 1 = \varphi^{-1}$ (golden-ratio recognition overhead per qubit), this is $0 < \varphi^{-1}$.
background
The module treats qubit channel capacity in Recognition Science units. Classically one qubit carries one bit; RS inserts a recognition overhead, so effective classical capacity is $\varphi^{-1}$ bits per qubit (about $0.618$). The constant $\varphi = (1+\sqrt{5})/2$ is the self-similar fixed point forced at T6 of the unified forcing chain.
The sibling definition canonicalThreshold is that overhead scale (equal to $\varphi-1$, hence to $\varphi^{-1}$). Positivity is the minimal arithmetic fact needed before certificates or capacity inequalities can mention the threshold as a positive scale.
Upstream, phi_gt_onePointFive supplies the tight lower bound $\varphi > 1.5$, obtained from $\sqrt{5} > 2$. That bound is stronger than $\varphi > 1$ and is exactly what linear arithmetic needs after unfolding.
proof idea
One-line wrapper. Unfold canonicalThreshold (exposing an affine expression in $\varphi$, namely $\varphi-1$), then apply linarith with the single lemma phi_gt_onePointFive ($1.5 < \varphi$). No further case splits or field lemmas are required.
why it matters
Gives the sign of the RS qubit overhead scale that the module advertises as structural (zero sorry, zero axiom). The module claim is that quantum channel capacity equals $\varphi^{-1}$ times qubit count; positivity of that factor is the first arithmetic gate before any certificate (QubitChannelCert, cert_inhabited) can treat the threshold as a genuine positive constant.
In the broader framework this is the same $\varphi^{-1}$ that appears as the Berry creation threshold. It sits downstream of T6 (φ forced) and of the Constants layer bound $\varphi > 1.5$. No used_by edges are recorded yet; the lemma is local scaffolding for the capacity certificate in this file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.