domainCost_at_eq
plain-language theorem explainer
Equal nonzero arguments make the domain cost vanish. Channel-capacity and qubit-overhead arguments in Recognition Science use this as the normalization that the cost of a perfect match is zero. The proof unfolds the cost to J of a ratio, collapses the ratio to 1, and quotes J(1)=0.
Claim. For every real number $r \neq 0$, the domain cost of the matched pair $(r,r)$ is zero.
background
This module treats qubit channel capacity in Recognition Science. Classically one qubit carries one classical bit; after recognition overhead the effective capacity is $\varphi^{-1}$ bits per qubit (about 0.618). Status is structural: no sorry, no axioms.
The cost $J$ is the unique nonnegative self-similar cost forced at T5: $J(x)=(x+x^{-1})/2-1$, equivalently $J(x)=(x-1)^2/(2x)$. It is zero exactly at the unit scale. Upstream, Jcost_unit0 records $J(1)=0$ by direct simplification of that formula.
Domain cost is the local cost of a ratio of two nonzero real scales. Unfolding shows it is $J$ applied to that ratio, so matched arguments reduce to the unit root of $J$.
proof idea
One-line wrapper. Unfold the domain-cost definition to expose $J(r/r)$. Rewrite the ratio to $1$ with div_self (using $r\neq 0$). Finish by exact Jcost_unit0, the lemma $J(1)=0$.
why it matters
Gives the zero-cost normalization for matched scales inside the qubit channel-capacity certificate. The module claims quantum channel capacity equals $\varphi^{-1}$ times qubit count after recognition overhead; this lemma is the algebraic base case that a perfect ratio costs nothing. Sibling results cover nonnegativity, the canonical threshold, and inhabitation of the capacity certificate. No downstream users appear in the graph yet, so the lemma is local infrastructure for that certificate. It sits under T5 J-uniqueness and the recognition composition law, both of which treat $J$ as the unique cost with $J(1)=0$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.