QECThresholdExactRS
plain-language theorem explainer
Packages three exact properties for the RS quantum-error-threshold certificate: domain cost vanishes on the diagonal, stays nonnegative for positive measurement and error rates, and the canonical threshold is strictly positive. Downstream code inhabits this record to certify the RS prediction p_th = J(φ)/10 ≈ 1.18%. Pure structure definition; no proof body.
Claim. A certificate record asserting: (i) for every nonzero real $r$, the domain cost at equal arguments vanishes, $\mathrm{cost}(r,r)=0$; (ii) for positive measurement and error rates $m,e>0$, $\mathrm{cost}(m,e)\ge 0$; (iii) the canonical QEC threshold is strictly positive.
background
The module states the Recognition Science 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).
Domain cost is the local cost functional on measurement/error rate pairs; the sibling lemmas assert it vanishes on the diagonal and is nonnegative off it. The canonical threshold is the positive RS scalar used as $p_{\mathrm{th}}$. Upstream, ObserverForcing records that every recognition-event cost is nonnegative via $J$-cost nonnegativity on positive states.
The structure is the interface that bundles those three facts into a single certificate type for the information-theoretic QEC claim.
proof idea
No proof body: this is a structure declaration. Its three fields are Prop-valued requirements (diagonal vanishing of domain cost, nonnegativity for positive rates, positivity of the canonical threshold). Inhabitation is deferred to the sibling cert, which fills the fields by the corresponding lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos.
why it matters
Gives the typed certificate that the module's inhabited witness (cert, cert_inhabited) must satisfy, locking the RS QEC threshold story to three checkable algebraic properties rather than a free-floating number. The module doc pins the physical claim: $p_{\mathrm{th}}=J(\varphi)/10\approx 1.18%$, with partial empirical pass against surface and color codes. Ties into the broader RS cost calculus ($J$-cost nonnegativity from ObserverForcing) and the $\varphi$-forced constants of the forcing chain, without yet deriving the factor $1/10$ from first principles inside this file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.