canonicalThreshold
plain-language theorem explainer
Defines the bare RS canonical threshold as φ − 3/2, equal to the J-cost J(φ) ≈ 0.118. Anyone citing the RS quantum-error-rate prediction p_th = J(φ)/10 ≈ 1.18% uses this constant as the un-normalized yardstick. The body is a one-line real definition, not a proved equality.
Claim. The canonical threshold is the real constant $\varphi - 3/2$, where $\varphi$ denotes the golden ratio (self-similar fixed point of Recognition Science).
background
The module fixes the Recognition Science prediction for the quantum-error-correction fault-tolerance threshold: $p_{\mathrm{th}} = J(\varphi)/10 \approx 1.18%$, compared with surface-code (~1.0%) and color-code (~1.1%) empirics.
Here $J$ is the unique cost functional forced by the Recognition Composition Law, $J(x) = (x + x^{-1})/2 - 1$. For the golden ratio one has the elementary identity $J(\varphi) = \varphi - 3/2$, so the present definition simply names that bare cost value before the conventional factor of $1/10$.
The surrounding file imports only Mathlib, the RS constants (including $\varphi$), and the cost module; no further hypotheses are required to introduce the constant.
proof idea
Pure definitional abbreviation: the real is set equal to $\varphi - 3/2$ in a single equation. No tactics, lemmas, or rewriting are involved.
why it matters
Supplies the un-normalized scale that the module’s exact threshold statement and certificate later divide by ten. In the broader RS chain it sits downstream of T5 (J-uniqueness) and T6 ($\varphi$ forced as self-similar fixed point): once those are in hand, $J(\varphi)$ collapses algebraically to $\varphi - 3/2$. The numerical target 1.18% is the structural RS prediction against which surface- and color-code thresholds are scored (RS_PARTIAL_PASS). Sibling positivity and exact-threshold lemmas build directly on this constant.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.