pith. machine review for the scientific record. sign in
def definition def or abbrev high

errorRateCost

show as:
view Lean formalization →

Error rate cost is defined as the J-cost of the ratio between actual and threshold error rates. Quantum error correction researchers cite it when bounding surface code fault-tolerance thresholds via Recognition Science cost. The definition is a direct one-line wrapper around the Jcost operator applied to the normalized rate.

claimThe cost of an actual error rate $r$ relative to a threshold $t$ is given by $J(r/t)$, where $J$ is the J-cost function satisfying $J(1)=0$ and $J(x)≥0$ for $x>0$.

background

The J-cost function is $J(x)=(x+x^{-1})/2-1$, the unique fixed-point deviation measure from the Recognition Composition Law and the T5 step of the forcing chain. This module applies it to physical error rates to obtain a cost measure for quantum error correction thresholds.

proof idea

The definition is a one-line wrapper that applies Jcost directly to the ratio of the two real inputs.

why it matters in Recognition Science

This definition supplies the cost measure used inside the ErrorCorrectionCert structure and its supporting theorems on zero cost at threshold and non-negativity. It realizes the Recognition Science prediction that the surface code threshold lies near J(φ)/10 ≈1.18% inside the 0.5-2% empirical band, linking the phi-ladder and eight-tick octave to quantum bounds with zero axioms.

scope and limits

formal statement (Lean)

  44def errorRateCost (actual_rate threshold_rate : ℝ) : ℝ :=

proof body

Definition body.

  45  Jcost (actual_rate / threshold_rate)
  46

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.