errorRateCost_at_threshold
The theorem establishes that the J-cost of the error rate ratio equals zero precisely when the actual rate matches the threshold rate for any nonzero real argument. Quantum error correction modelers working in the Recognition Science framework would cite this to fix the zero point of the cost function. The proof is a one-line wrapper that unfolds the definition, cancels the ratio, and applies the J-cost unit lemma.
claimFor any nonzero real number $r$, the J-cost of the ratio of actual error rate to threshold rate is zero when the two rates coincide: $J(r/r)=0$.
background
The module develops the Recognition Science account of surface-code fault tolerance by expressing the cost of an error rate as the J-cost of its ratio to the threshold. The upstream lemma Jcost_unit0 states that Jcost(1)=0 and follows from the algebraic definition Jcost(x)=(x-1)^2/(2x). This sits inside the structural theorem for the quantum error-correction threshold, whose module doc records the RS prediction J(φ)/10 ≈1.18% and the empirical band 0.5-2%.
proof idea
The proof is a one-line wrapper. It unfolds errorRateCost to obtain Jcost(r/r), rewrites the ratio to 1 via div_self (using r≠0), and applies the lemma Jcost_unit0.
why it matters in Recognition Science
The result supplies the cost_at_threshold field required by the downstream ErrorCorrectionCert definition. It anchors the zero-cost point that supports the RS surface-code threshold claim J(φ)/10 and connects to the J-uniqueness step (T5) in the forcing chain. The module doc lists the concrete falsifier: any surface-code implementation with threshold outside (0.1%,2%).
scope and limits
- Does not compute a numerical threshold value.
- Does not address error models outside the J-cost ratio.
- Does not prove existence of a fault-tolerant code.
- Does not treat finite-size or correlated errors.
formal statement (Lean)
47theorem errorRateCost_at_threshold (r : ℝ) (h : r ≠ 0) :
48 errorRateCost r r = 0 := by
proof body
One-line wrapper that applies unfold.
49 unfold errorRateCost; rw [div_self h]; exact Jcost_unit0
50