errorRateCost
plain-language theorem explainer
The definition assigns to each pair of actual and threshold error rates the J-cost of their ratio. Researchers modeling fault-tolerant quantum computation with surface codes would reference this when deriving the recognition-science bound on the threshold. The definition is a direct application of the J-cost function to the normalized rate ratio.
Claim. For actual error rate $a$ and threshold error rate $t$, the error-rate cost is given by $J(a/t)$, where $J$ denotes the J-cost function.
background
The J-cost function, imported from the Cost module, quantifies the recognition cost of a deviation ratio via the Recognition Composition Law. This module applies the cost to quantum error correction, with the module document stating the RS prediction that the surface code fault-tolerance threshold lies near $J(φ)/10 ≈ 1.18$ percent and is consistent with the empirical band of 0.5 to 2 percent. The local theoretical setting is the construction of an error-correction certificate that encodes positivity of the threshold together with non-negativity of the cost at and above threshold.
proof idea
This is a one-line definition that applies the Jcost function to the ratio of the two input rates.
why it matters
This definition supplies the cost measure used inside the ErrorCorrectionCert structure, which records that the threshold is positive, that the cost vanishes exactly at threshold, and that the cost is nonnegative for positive rates. It supports the RS claim linking the surface-code threshold to the J-function evaluated at the golden ratio and to the eight-tick octave structure. It touches the open question of tightening the predicted interval (0.5-2 percent) against future experimental data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.