domainCost_at_eq
plain-language theorem explainer
On the diagonal, domain cost vanishes: for any nonzero real r the cost of r against itself is zero. Cost-calculus and threshold arguments in the RS structural modules cite this as the normalization identity. The proof unfolds the cost to J(r/r), rewrites the ratio to 1, and applies Jcost_unit0.
Claim. For every real number $r \neq 0$, the domain cost of $r$ against itself is zero: if $\mathrm{domainCost}(x,y) := J(x/y)$ with $J$ the RS cost, then $\mathrm{domainCost}(r,r) = 0$.
background
The RS cost is the unique symmetric convex functional fixed by the Recognition Composition Law; in closed form $J(x)=(x+x^{-1})/2-1$, equivalently $J(x)=(x-1)^2/(2x)$ for $x>0$. It vanishes only at the unit: $J(1)=0$ (lemma Jcost_unit0).
In this module the two-argument domain cost is the pullback of $J$ along the ratio map, so comparing a scale to itself is exactly $J(1)$. The module sits in the structural forcing chain (T5 J-uniqueness through T8 dimension three) and is marked fully proved: zero sorry, zero axiom.
Upstream, Jcost_unit0 is the one-point evaluation that every diagonal identity reduces to.
proof idea
One-line wrapper. Unfold the definition of domain cost (which is $J$ of the ratio of the two arguments). Rewrite $r/r=1$ by div_self using the hypothesis $r\neq 0$. Finish by exact application of Jcost_unit0, which states $J(1)=0$.
why it matters
Supplies the diagonal normalization for the domain-cost calculus used throughout RS_MTH_Structural_009 (siblings include domainCost_nonneg and the canonical threshold package). Without cost-zero on equal arguments, nonnegativity and threshold positivity would lack their base case.
In the forcing chain this is bookkeeping under T5 (J-uniqueness): once $J$ is fixed, every derived cost must recover the same unit zero. No downstream theorems currently list this lemma as a dependency in the graph, so it functions as a local structural fact inside the module certificate rather than a widely re-exported primitive.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.