domainCost_at_eq
plain-language theorem explainer
When both arguments of the domain cost are the same nonzero real, the cost is exactly zero. Anyone normalizing the RS quantum-error threshold off the J-cost cites this equal-scale baseline. The proof is a one-line unfold of the ratio definition, then the unit identity J(1)=0.
Claim. For every real $r\neq 0$, the domain cost of the pair $(r,r)$ is zero. (Unfolding, the domain cost is the $J$-cost of the ratio of its two inputs, so the claim is $J(r/r)=J(1)=0$.)
background
This module states the Recognition Science quantum-error-correction threshold prediction $p_{\mathrm{th}}=J(\varphi)/10\approx 1.18%$, set against surface-code (~1.0%) and color-code (~1.1%) empirics, and marks the development as a structural theorem (no sorry, no axioms).
The underlying cost is the RS $J$-functional forced by the Recognition Composition Law (forcing step T5): $J(x)=(x+x^{-1})/2-1$, equivalently $J(x)=(x-1)^2/(2x)$, with the unit normalization $J(1)=0$. In this file the domain cost of two nonzero scales is that $J$-cost applied to their ratio.
The only upstream fact used is the Cost-module lemma that $J(1)=0$.
proof idea
One-line wrapper. Unfold the domain-cost definition to expose $J$ of the ratio of the two arguments; rewrite $r/r=1$ by the field identity div_self (using $r\neq 0$); finish by the Cost lemma $J(1)=0$.
why it matters
Gives the equal-argument normalization for the domain cost that the rest of the QEC-threshold development sits on. Sibling results in the same module (nonnegativity of domain cost, the canonical threshold and its positivity, and the exact RS QEC threshold certificate) treat zero cost at matched scales as the baseline against which error rates are measured. The numerical RS claim $p_{\mathrm{th}}=J(\varphi)/10\approx 1.18%$ is the module-level target; this lemma is the local $J(1)=0$ step inside that structural package. It sits under T5 $J$-uniqueness in the forcing chain. The dependency graph currently shows no external used-by edges, so the lemma is internal to the threshold certificate rather than a cross-module export.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.