canonicalThreshold_pos
plain-language theorem explainer
The RS canonical quantum-error-correction threshold is strictly positive. Anyone quoting the fault-tolerance prediction p_th = J(φ)/10 ≈ 1.18% needs this elementary positivity fact first. The proof unfolds the definition and finishes by linear arithmetic from the bound φ > 1.5.
Claim. The canonical RS quantum error-correction threshold satisfies $0 < p_{\mathrm{th}}$, where $p_{\mathrm{th}}$ is defined from the J-cost at the golden ratio (module convention: $p_{\mathrm{th}} = J(\varphi)/10$).
background
The module fixes the RS quantum error-rate prediction: the fault-tolerance threshold is $p_{\mathrm{th}} = J(\varphi)/10 \approx 1.18%$, compared with empirical surface-code (~1.0%) and color-code (~1.1%) values. Status is structural (zero sorry, zero axiom).
Here $J$ is the unique nonnegative cost forced by the Recognition Composition Law and T5 uniqueness, $J(x) = (x+x^{-1})/2-1$. The scale $\varphi$ is the self-similar fixed point from T6. The sibling definition canonicalThreshold packages that $J(\varphi)/10$ quantity.
The only upstream fact used is the elementary bound $\varphi > 1.5$, obtained from $\sqrt{5} > 2$.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then invoke linarith on the lemma $\varphi > 1.5$. Positivity of the unfolded expression follows at once from that strict lower bound on $\varphi$.
why it matters
Positivity is the first sanity check on the RS QEC threshold before any numerical or comparative claim. The module advertises $p_{\mathrm{th}} = J(\varphi)/10 = 1.18%$ as the RS prediction (RS_PARTIAL_PASS against surface and color codes). Sibling certificates and the exact-threshold statement sit on top of this fact. It touches the T5/T6 landmarks (unique J-cost and forced $\varphi$) but does not itself derive the 1.18% figure or the empirical match.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.