canonicalThreshold_pos
plain-language theorem explainer
The canonical recognition threshold is strictly positive. RS information and channel-capacity arguments cite this to keep coupling scales and reciprocal factors well-defined. The proof is a one-line wrapper: unfold the threshold, then linear arithmetic from φ > 1.5.
Claim. The canonical recognition threshold is strictly positive: $0 < \tau_{\mathrm{can}}$, where $\tau_{\mathrm{can}}$ is the threshold constant used at the canonical recognition coupling in the RS information layer.
background
This module develops RS information structure for quantum channel capacity. The standing claim is structural: $Q = \max_{\phi_A} I(A;B)$ specializes in RS to $Q = J(\varphi)^{-1}$ times classical capacity at the canonical recognition coupling, with no sorry and no extra axioms.
The golden ratio $\varphi = (1+\sqrt{5})/2$ is the self-similar fixed point forced upstream in the T5–T6 segment of the forcing chain. The only upstream fact used here is the tighter real bound $\varphi > 1.5$, obtained from $\sqrt{5} > 2$.
Sibling definitions in the same file introduce domain cost, the canonical threshold itself, and a four-deep capacity certificate. Positivity of the threshold is the elementary real inequality that keeps those constructions on the positive side of the cost and coupling scales.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then discharge the resulting real inequality by linarith using the lemma $\varphi > 1.5$. No case split and no further Recognition identities are required.
why it matters
Positivity is the minimal well-formedness fact for the canonical coupling scale in the RS information layer. The module frames quantum capacity as $Q = J(\varphi)^{-1}$ times classical capacity at that coupling; a non-positive threshold would collapse reciprocal factors and cost normalizations tied to $J$ and $\varphi$.
No downstream consumers are wired yet in the graph, so this is infrastructure rather than a cited lemma in a larger proved theorem. It sits next to domain-cost non-negativity and the capacity certificate siblings, and it inherits $\varphi$ from the Constants layer (T6 fixed-point force). It does not itself prove the capacity identity; it only secures the sign of the threshold constant those arguments will use.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.