cert_inhabited
plain-language theorem explainer
The RS quantum error-correction threshold certificate is inhabited: a single package witnesses diagonal vanishing of domain cost, nonnegativity for positive arguments, and positivity of the canonical threshold. Anyone citing the RS prediction p_th = J(φ)/10 ≈ 1.18% against surface/color-code empirics relies on this inhabitation. Proof is a one-line term exhibiting the prebuilt certificate.
Claim. The type of RS quantum-error-correction threshold certificates is nonempty: there exists a witness packing (i) $\mathrm{domainCost}(r,r)=0$ for all $r\neq 0$, (ii) $\mathrm{domainCost}(m,e)\ge 0$ whenever $m>0$ and $e>0$, and (iii) the canonical threshold is strictly positive.
background
This module packages the Recognition Science prediction for the QEC fault-tolerance threshold: $p_{\mathrm{th}}=J(\varphi)/10\approx 1.18%$, compared with empirical surface-code (~1.0%) and color-code (~1.1%) thresholds. Status is structural (zero sorry, zero axiom) and marked RS_PARTIAL_PASS.
The certificate structure bundles three elementary properties of the local cost. Domain cost is the RS cost functional evaluated on a mass/error pair; it is required to vanish on the diagonal (equal arguments, nonzero) and to be nonnegative for positive mass and error. The canonical threshold is the positive real that the module identifies with $J(\varphi)/10$, where $J(x)=(x+x^{-1})/2-1$ is the unique cost forced by the Recognition Composition Law (T5).
Upstream, the structure itself only declares the three fields; the concrete lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos (siblings in the same file) discharge them and are assembled into the named certificate used here.
proof idea
Pure term proof. Nonempty is inhabited by the anonymous constructor ⟨cert⟩, where cert is the prebuilt structure value that already fills the three fields (diagonal vanishing, nonnegativity, threshold positivity). No tactics, no further lemmas.
why it matters
Gives a single inhabitation fact for the whole RS QEC-threshold certificate, so downstream developments can assume the package rather than re-prove the three cost properties. The module frames this as the structural backbone of the $p_{\mathrm{th}}=J(\varphi)/10$ prediction (T5 J-uniqueness, $\varphi$ from T6). No used_by edges yet; the declaration is the terminal inhabitation step inside the module. It does not close the empirical gap to surface/color codes; it only certifies that the RS-side inequalities and positivity are realized.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.