cert
plain-language theorem explainer
cert assembles an explicit certificate for the surface-code fault-tolerance threshold by supplying its positivity, the vanishing of the associated J-cost when physical and threshold rates coincide and are nonzero, and the nonnegativity of that cost for positive rates. A quantum information theorist studying fault-tolerant thresholds would cite it to embed the Recognition Science J-cost prediction inside the observed 1% band. The construction is a direct record literal that invokes three upstream lemmas on positivity and cost properties.
Claim. The definition supplies an instance of the error-correction certificate structure asserting that the surface-code threshold $p_{th}$ satisfies $0 < p_{th}$, that the J-cost of the error rate vanishes when the physical error rate equals the threshold rate (and is nonzero), and that the J-cost of the error rate is nonnegative whenever both rates are positive.
background
In the Recognition Science treatment of quantum error correction the J-cost measures the recognition cost of an event and is nonnegative by the theorem cost_nonneg from ObserverForcing. The error-rate cost is obtained by applying this J-cost to the ratio of physical error rate to threshold rate. The module establishes a structural theorem with zero axioms that predicts the surface-code threshold near J(φ)/10 ≈ 1.18%, consistent with the empirical 1% value and the RS band (0.5-2%). The certificate structure requires three properties: positivity of the threshold, vanishing of the cost at equal nonzero rates, and nonnegativity of the cost for positive arguments. These are supplied by the lemmas on threshold positivity, cost vanishing at threshold, and cost nonnegativity.
proof idea
The definition is a one-line record construction that populates the three fields of the error-correction certificate using the positivity of the surface-code threshold, the vanishing of the error-rate cost when rates are equal and nonzero, and the nonnegativity of the error-rate cost for positive arguments. It directly applies the three upstream results on these properties without further computation.
why it matters
This definition completes the structural theorem for the quantum error-correction threshold in the Recognition Science framework by exhibiting an explicit certificate. It supports the module's claim of a zero-axiom structural result linking the J-cost to the surface-code threshold near 1.18%. The result sits inside the quantum-computing domain and provides a concrete falsifiable prediction for fault-tolerance thresholds, with the module documenting the falsifier as any surface-code implementation outside the 0.1-2% band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.