domainCost_at_eq
plain-language theorem explainer
Equal nonzero scale arguments give vanishing domain cost. Cosmology workers in the RS structural stack cite this as the zero-defect baseline on the diagonal. The proof unfolds the cost to J of a ratio, cancels that ratio to 1, and applies the unit root of J.
Claim. For every real $r \neq 0$, the domain cost of the pair $(r,r)$ vanishes: if the cost is $J$ of the ratio of the two arguments, then that value is $0$.
background
Module RS_COS_Structural_001 records structural cosmology predictions forced by Recognition Science: the cost $J(x)=\frac12(x+1/x)-1$, the golden ratio fixed point, and $D=3$. Status is a structural theorem block (no sorry, no axioms).
The Recognition cost $J$ (written Jcost upstream) is nonnegative on positive reals and vanishes only at the unit. Upstream lemma Jcost_unit0 states $J(1)=0$, equivalently from the squared-ratio form $J(x)=(x-1)^2/(2x)$. In this module the domain cost of a pair of real scales is that $J$ applied to their ratio, so the diagonal case reduces to the unit root once the ratio is defined.
proof idea
One-line wrapper. Unfold the domain-cost definition to expose $J$ of the ratio of the two arguments; rewrite that ratio by div_self using $r\neq 0$ to obtain $J(1)$; finish with the upstream lemma $J(1)=0$.
why it matters
Supplies the diagonal vanishing identity for the cosmology domain cost inside RS_COS_Structural_001. Sibling facts in the same file (nonnegativity of domain cost, positivity of the canonical threshold, and the structural certificate) rest on a clean zero when the two scales match. Framework-wise this is the local instance of T5 J-uniqueness: $J$ is the unique cost compatible with the Recognition Composition Law, and $J(1)=0$ is its normalization. No downstream dependents are recorded yet; the lemma is infrastructure for later structural comparisons rather than a bridge to observational fits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.