canonicalThreshold
plain-language theorem explainer
Defines the real threshold φ − 3/2 used as the canonical cutoff in the J-cost channel-capacity development. Anyone citing the structural Shannon link C = B log₂(1+SNR) at the RS operating point will pull this constant. It is a bare definitional abbreviation of the golden-ratio shift, not a proved inequality.
Claim. The canonical threshold is the real number $\varphi - 3/2$, where $\varphi$ is the golden ratio (self-similar fixed point of the Recognition forcing chain).
background
The module derives a structural form of Shannon channel capacity from the Recognition J-cost. In RS units the operating SNR is fixed at $J(\varphi)^{-2}\approx 71.7$, which yields $C=B\log_2(72.7)\approx B\cdot 6.18$ bits/s/Hz, noted as structurally near $\varphi^{2\varphi}$.
$J$ is the unique cost $J(x)=(x+x^{-1})/2-1$ forced by T5; $\varphi$ is the self-similar fixed point forced by T6. The present constant is a simple real shift of $\varphi$ that appears as a named threshold in the local capacity certificate (alongside nonnegativity of the domain cost).
proof idea
Pure definition: the real constant is introduced by the equation $\varphi-3/2$. No proof obligations, tactics, or upstream lemmas are involved.
why it matters
Gives a single named real for the cutoff that the channel-capacity certificate and its positivity lemma refer to. It sits inside the Information domain’s structural Shannon link (Plan v7 session 3), tying the classical $C=B\log_2(1+\mathrm{SNR})$ formula to the RS J-cost at the forced $\varphi$ scale. Downstream siblings such as the positivity statement for this threshold and the inhabited capacity certificate use it as the reference level. It does not itself close a forcing-chain step (T0–T8); it is local scaffolding for the capacity identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.