errorRateCost_nonneg
Non-negativity of the error rate cost follows from non-negativity of J-cost applied to the ratio of actual to threshold error rates. Quantum error correction researchers modeling surface code thresholds in Recognition Science would cite this when confirming consistency with the predicted 1.18% band. The proof is a one-line wrapper that unfolds the definition and invokes the established Jcost non-negativity lemma on the positive quotient.
claimFor $a > 0$ and $t > 0$, $0 ≤ J(a/t)$, where $J(x) = (x + x^{-1})/2 - 1$.
background
The module defines error rate cost as J-cost of the ratio of actual error rate to threshold rate. J-cost satisfies $J(x) ≥ 0$ for $x > 0$ by the AM-GM inequality $x + x^{-1} ≥ 2$, as shown in upstream lemmas such as Jcost_nonneg from the Cost module and parallel statements in Gravity and Navier-Stokes modules. The local setting is the Recognition Science prediction that the surface code fault-tolerance threshold lies near $J(φ)/10 ≈ 1.18%$, consistent with the empirical band 0.5-2%.
proof idea
One-line wrapper that unfolds errorRateCost to expose Jcost of the ratio and applies Jcost_nonneg to the positive quotient produced by div_pos.
why it matters in Recognition Science
The result supplies the cost_nonneg field for the ErrorCorrectionCert definition in the same module. It completes the non-negativity component required for the quantum computing application of the J-cost framework, paralleling its use in gravity and fluid modules. The declaration supports the structural claim that the surface code threshold remains inside the RS band (0.5, 2)%.
scope and limits
- Does not compute the numerical value of the surface code threshold.
- Does not derive the J-cost function or its fixed-point properties.
- Does not address quantum error correction codes beyond cost non-negativity.
- Does not supply bounds tighter than the module falsifier interval.
Lean usage
have h : 0 ≤ errorRateCost a t := errorRateCost_nonneg a t ha htformal statement (Lean)
51theorem errorRateCost_nonneg (a t : ℝ) (ha : 0 < a) (ht : 0 < t) :
52 0 ≤ errorRateCost a t := by
proof body
One-line wrapper that applies unfold.
53 unfold errorRateCost; exact Jcost_nonneg (div_pos ha ht)
54