domainCost_at_eq
plain-language theorem explainer
The domain cost vanishes on the diagonal: for any nonzero real r, comparing r to itself costs zero under J. Scale-ratio and cost-functional arguments in Recognition Science cite this as the baseline identity. The proof is a one-line unfold that rewrites the self-ratio to 1 and applies J(1)=0.
Claim. For every real $r \neq 0$, the domain cost of the pair $(r,r)$ is zero. Equivalently, if the domain cost is $J$ applied to the ratio of its arguments, then $J(r/r)=0$.
background
The Recognition cost $J$ is the unique symmetric cost fixed by the Recognition Composition Law. Explicitly $J(x)=(x+x^{-1})/2-1$, or in squared-ratio form $J(x)=(x-1)^2/(2x)$ for $x>0$. It is normalized so that the unit ratio is free: $J(1)=0$.
This module records structural mathematics around the RS gap-45 identity $D^2(D+2)=9\cdot 5=45$ at spatial dimension $D=3$, described as the minimum rung for stable self-reference. The domain cost is the local cost of a scale comparison: feed the quotient of the two arguments into $J$.
The sole upstream fact used here is the unit lemma $J(1)=0$, obtained by direct simplification of the definition of $J$.
proof idea
One-line wrapper. Unfold the domain-cost definition to expose $J(r/r)$. Rewrite the self-quotient to $1$ with the nonzero hypothesis, then apply the unit lemma $J(1)=0$.
why it matters
Gives the diagonal vanishing law for the domain cost: any scale compared to itself carries zero recognition cost. That is the normalization baseline for every later inequality or threshold built on the same cost.
The ambient module is the structural layer for gap-45 (minimum rung for stable self-reference at $D=3$). No downstream dependents are recorded yet; sibling facts in the same file cover nonnegativity of the domain cost and the canonical threshold. In the broader forcing chain this sits under T5 ($J$-uniqueness) and the self-similar fixed-point story at T6, without itself proving those steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.