errorRateCost
plain-language theorem explainer
errorRateCost defines the J-cost applied to the ratio of actual physical error rate to threshold rate for quantum error correction. Quantum information researchers using Recognition Science cite it to bound surface-code fault-tolerance thresholds. The definition is a direct one-line application of the Jcost operator to the normalized rate ratio.
Claim. The error-rate cost is defined by $J(r/t)$ where $r$ is the actual error rate, $t$ the threshold rate, and $J$ is the J-cost function satisfying the Recognition Composition Law.
background
The module derives quantum error-correction thresholds from J-cost. J-cost is the function $J(x)=(x+x^{-1})/2-1$ that satisfies the Recognition Composition Law and appears in the phi-ladder mass formula. The local setting is the structural claim that the surface-code threshold lies near $J(φ)/10≈1.18%$, inside the empirical band 0.5-2%.
proof idea
One-line definition that applies Jcost directly to the quotient of the two real arguments.
why it matters
Supplies the cost measure inside ErrorCorrectionCert, which records threshold positivity, zero cost at equality, and non-negativity. It anchors the Recognition Science prediction of an ≈1% surface-code threshold consistent with the eight-tick octave and phi-ladder. The module falsifier is any surface-code implementation whose threshold lies outside 0.1-2%.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.