cert
plain-language theorem explainer
Packages the three structural facts needed for the RS quantum-error-threshold certificate: domain cost vanishes on the diagonal, is nonnegative off it, and the canonical threshold is positive. Anyone citing the RS prediction p_th = J(φ)/10 ≈ 1.18% uses this inhabitant. The body is a pure structure instance wiring three already-proved sibling lemmas.
Claim. There exists a certificate of the RS exact QEC threshold consisting of: (i) $\mathrm{domainCost}(r,r)=0$ for all $r\neq 0$; (ii) $\mathrm{domainCost}(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) the canonical threshold is strictly positive.
background
The module fixes the RS quantum-error-rate claim: 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).
domainCost is the two-argument cost on measurement/error ratios built from the RS J-cost $J(x)=(x+x^{-1})/2-1$. The structure QECThresholdExactRS packages the three algebraic properties any exact-threshold certificate must carry: vanishing on equal arguments, nonnegativity for positive arguments, and positivity of canonicalThreshold.
Upstream, nonnegativity of recognition cost is already forced in ObserverForcing (cost_nonneg: "The cost of any recognition event is non-negative"), via Jcost_nonneg at positive state.
proof idea
One-line structure instance. The three fields of QECThresholdExactRS are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively. No new arithmetic is performed; the definition only assembles those proofs into a single certificate value.
why it matters
Gives a single named inhabitant of the exact-threshold structure that the module advertises as the RS QEC prediction $p_{\mathrm{th}}=J(\varphi)/10$. That prediction sits on the J-uniqueness landmark (T5) and the forced self-similar scale $\varphi$ (T6). The module marks the comparison with surface/color codes as RS_PARTIAL_PASS (7/8 codes within 20%).
No downstream theorems currently depend on this certificate (used_by is empty), but the sibling cert_inhabited witnesses that the type is nonempty. The declaration closes the structural side of the threshold claim without introducing axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.