domainCost
plain-language theorem explainer
Defines the domain cost of a measurement-to-error ratio as the RS recognition cost J(m/e). Used in the quantum-error-rate module to build the fault-tolerance threshold p_th = J(φ)/10 ≈ 1.18%. Pure abbreviation: apply the unique J-cost to the positive ratio of two reals.
Claim. For real numbers $m$ and $e$, the domain cost is $J(m/e)$, where $J(x) = \frac{1}{2}(x + x^{-1}) - 1$ is the recognition cost of a positive ratio.
background
The module predicts a quantum error-correction fault-tolerance threshold $p_{\mathrm{th}} = J(\varphi)/10 \approx 1.18%$, compared with empirical surface-code (~1.0%) and color-code (~1.1%) values. Status is structural (no sorry, no axioms).
The recognition cost $J$ is the unique functional forced by the Recognition Composition Law: $J(x) = \frac{x+x^{-1}}{2}-1$ (equivalently $\cosh(\log x)-1$). Upstream docs state it is the RS cost of a positive ratio, strictly positive when the ratio is not one, and non-negative for $x>0$. Domain cost simply evaluates that functional on the ratio of two reals $m$ and $e$ (measurement scale over error scale).
proof idea
One-line definitional abbreviation. No tactics or lemmas: the body is exactly $J(m/e)$ with $J$ the standard recognition cost imported from Cost (and re-exported in several modules).
why it matters
Supplies the cost primitive for the RS quantum-error-rate stack. Sibling results (non-negativity, evaluation at equality, the canonical threshold, and the exact QEC threshold certificate) build on this ratio cost. It ties the information-theoretic threshold to the T5 J-uniqueness landmark and to $\varphi$ via the module claim $p_{\mathrm{th}}=J(\varphi)/10$. No downstream users are recorded yet outside the module siblings; the definition is the local yardstick that makes the 1.18% prediction well-typed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.