canonicalThreshold
plain-language theorem explainer
Defines the canonical LDPC rate-gap threshold as φ − 3/2 (≈ 0.118). That value is exactly the J-cost at the golden-ratio fixed point, the structural capacity penalty used in this module. Coding theorists tying finite-blocklength LDPC gaps to Recognition cost would cite it. The body is a one-line real definition.
Claim. The canonical threshold is the real constant $\varphi - 3/2$, where $\varphi$ is the self-similar fixed point of the Recognition forcing chain.
background
This module treats LDPC code-rate gaps as instances of Recognition J-cost. The cost functional forced at T5 is $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), and $\varphi$ is the unique self-similar fixed point forced at T6.
A short algebraic identity gives $J(\varphi)=\varphi-3/2$: the golden-ratio relation $\varphi=1+1/\varphi$ implies $\varphi+\varphi^{-1}=2\varphi-1$, so $J(\varphi)=\varphi-3/2\approx 0.118$. The module status note records the empirical claim that well-designed LDPC codes sit within about 5–15% of Shannon capacity, matching this scale.
Sibling material in the same file (domain cost, nonnegativity, positivity of the threshold, and an LDPC certificate type) treats this constant as the design gap between target rate and capacity.
proof idea
Pure definition: the real is introduced by the closed form $\varphi-3/2$. No tactics, no lemmas, no proof obligations. Downstream positivity or certificate lemmas simply unfold this abbreviation.
why it matters
Pins the numerical LDPC capacity penalty used throughout the information layer to the same $J(\varphi)$ that appears in the forcing chain (T5 J-uniqueness, T6 $\varphi$). The module frames the structural theorem that practical LDPC codes pay a gap of order $J(\varphi)\approx 0.118$ rather than an ad-hoc engineering margin.
No downstream edges are recorded for this declaration itself; siblings such as the positivity lemma and the LDPC certificate inhabit the same constant. It does not close an open forcing step, but it makes the coding-theoretic reading of $J$ concrete and citable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.