canonicalThreshold_pos
plain-language theorem explainer
The canonical RS bandwidth threshold is a strictly positive real. Anyone using the phi-resonance Shannon capacity setup needs this positivity so logs and SNR remain well-defined. The proof is a one-line unfold-plus-linarith wrapper off the elementary bound φ > 1.5.
Claim. The canonical RS bandwidth threshold $\tau$ (the phi-derived constant used as the structural SNR/capacity threshold in this module) satisfies $0 < \tau$.
background
This module treats Shannon channel capacity $C = B\log_2(1+\mathrm{SNR})$ in Recognition Science units. At phi-resonance the structural SNR is identified with $\varphi^D = \varphi^3$ (with $D=3$), giving $C_{\mathrm{RS}} = B\log_2(\varphi^3+1)$. The golden ratio $\varphi = (1+\sqrt{5})/2$ is the self-similar fixed point forced earlier in the chain (T6).
The canonical threshold is the module's named positive real built from $\varphi$ that anchors that structural comparison. The only upstream fact required here is the elementary lower bound $\varphi > 1.5$, proved from $\sqrt{5} > 2$.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then discharge $0 < \tau$ by linarith using the imported lemma $\varphi > 1.5$. No further case splits or RS-specific identities are needed once the definition is expanded.
why it matters
Positivity is the minimal well-formedness fact for the structural bandwidth certificate in this file (siblings such as BandwidthPhiCert and the inhabited cert). It sits under the Information domain of the RS mirror and inherits $\varphi$ from the forcing chain (T6) and the eight-tick / $D=3$ octave (T7–T8) that fix $\varphi^3$ as the resonance SNR. The module is marked structural (0 sorry, 0 axiom); this lemma closes the positivity obligation so capacity expressions stay in the positive reals. No downstream consumers are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.