canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold constant in the J-cost channel-capacity module is strictly positive. Anyone building or citing the structural Shannon-capacity certificate at the RS-native SNR needs this to keep rates and logarithms well-defined. The argument is a one-line unfold of the threshold definition, then linear arithmetic from the bound φ > 1.5.
Claim. The canonical threshold is strictly positive: $0 < t_{\mathrm{can}}$, where $t_{\mathrm{can}}$ is the module's threshold constant defined from the golden ratio $\varphi$.
background
This module derives a structural Shannon channel-capacity statement from the RS cost functional. In ordinary units one has $C = B \log_2(1+\mathrm{SNR})$; the RS claim is that the distinguished operating point $\mathrm{SNR} = J(\varphi)^{-2} \approx 71.7$ yields $C/B = \log_2(72.7) \approx 6.18$ bits/s/Hz, comparable to $\varphi^{2\varphi}$.
Here $J$ is the unique nonnegative cost forced by the Recognition Composition Law (forcing step T5), $J(x) = (x+x^{-1})/2 - 1$, and $\varphi$ is the self-similar fixed point (T6). The canonical threshold is the module-local constant built from $\varphi$ that anchors that operating point and the subsequent capacity certificate.
The only upstream fact required for positivity is the elementary bound $\varphi > 1.5$, obtained from $\sqrt{5} > 2$ so that $(1+\sqrt{5})/2 > 3/2$.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then discharge the resulting linear inequality by linarith using the lemma $\varphi > 1.5$. No further cost identities or channel lemmas are invoked.
why it matters
Positivity of the canonical threshold is a gate for the structural capacity certificate assembled in this same module (the ChannelCap2Cert / inhabited-certificate siblings). Without $t_{\mathrm{can}} > 0$ the log-capacity expression and the comparison to the $\varphi$-ladder scale are not even well-posed as real inequalities.
The parent narrative is the Plan-v7 claim that ordinary Shannon capacity at one RS-native SNR is forced by J-cost geometry alone, with no external noise model. That sits downstream of T5 (J-uniqueness) and T6 ($\varphi$ fixed point) and supplies an information-theoretic reading of the same constants that appear in the mass ladder and the eight-tick octave. No external dependents are recorded yet; the lemma is local scaffolding for the module certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.