domainCost_at_eq
plain-language theorem explainer
When both domain arguments are the same nonzero real, the domain recognition cost is exactly zero. Cosmology structural certificates cite this to fix the diagonal of the cost surface. The argument unfolds the cost, collapses the ratio to one, and applies the unit root of J.
Claim. For every real $r \neq 0$, the domain recognition cost of the pair $(r,r)$ equals $0$.
background
This module packages structural facts about Recognition Science J-cost in a cosmology setting. The module states that recognition cost is ratio-symmetric: $J(x)=J(1/x)$, with status a fully proved structural theorem (no sorry, no axiom).
The domain cost is the J-cost of a ratio of two real domain parameters. The underlying cost is the standard RS functional $J$, equivalently written $J(x)=(x-1)^2/(2x)$ on the positive reals (and extended by the usual reciprocal symmetry). A basic root of that cost is the unit value: $J(1)=0$.
The local claim is the diagonal case of domain cost: feeding the same nonzero scale into both slots must yield zero cost, because the ratio collapses to one.
proof idea
One-line wrapper. Unfold the definition of domain cost so the goal is a statement about $J$ of a ratio; rewrite the ratio $r/r$ to $1$ using the nonzero hypothesis; finish by the upstream lemma that $J(1)=0$.
why it matters
Pins the zero set of domain cost on the diagonal, which is the minimal sanity check before any threshold or certificate that treats domain cost as a nonnegative defect. In the RS forcing chain this rests on T5 J-uniqueness: the same $J$ that solves the Recognition Composition Law and forces $\phi$ is the cost used here, so vanishing at unit ratio is not an extra axiom.
No downstream theorem edges are recorded for this declaration; it sits among the module siblings that build the structural certificate for cosmology module 7 (nonnegativity of domain cost, the canonical threshold, and the inhabited certificate bundle). Those siblings need the diagonal zero to keep the cost surface calibrated before comparing against positive thresholds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.