domainCost_at_eq
plain-language theorem explainer
On the D=3 recognition configuration space, the domain cost of any nonzero real against itself is zero. Metric and positivity arguments for the J-cost Riemannian structure cite this diagonal identity. The proof is a one-line unfold that reduces the ratio to 1 and applies J(1)=0.
Claim. For every real $r \neq 0$, the domain cost of $r$ relative to itself vanishes: evaluating the J-cost on the ratio $r/r$ yields $0$.
background
The module treats configuration space at $D=3$: $C_3=\mathbb{R}^3$ with the recognition metric $ds^2=J(dx/x)$ on the positive orthant. Status is structural (no sorry, no axioms). The cost $J$ is the unique functional forced by the Recognition Composition Law, $J(x)=(x+x^{-1})/2-1$, also written $\cosh(\log x)-1$; it is positive definite for $x>0$ and vanishes only at the identity ratio.
Domain cost is the pointwise J-evaluation on a ratio of scales (or coordinates). The sole upstream fact used here is $J(1)=0$, recorded as the unit lemma for the cost: at ratio one the squared-ratio form $J(x)=(x-1)^2/(2x)$ is identically zero.
proof idea
One-line wrapper. Unfold the definition of domain cost (J of the ratio), rewrite $r/r=1$ by the nonzero division identity, and finish with the unit lemma $J(1)=0$.
why it matters
Gives the diagonal vanishing law for the recognition metric on $C_3$, the minimal sanity check that self-distance is zero before nonnegativity and threshold lemmas in the same module. Sits inside the structural D=3 package tied to forcing-chain step T8 (three spatial dimensions). No downstream dependents are wired yet; the result is local infrastructure for the configuration-space certificate and for any later argument that treats domain cost as a genuine distance-like cost on ratios.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.