domainCost_at_eq
plain-language theorem explainer
For any nonzero real scale r, the domain cost of matching r against itself is exactly zero. Fine-structure and ladder-normalization arguments in the RS physics modules cite this as the diagonal baseline of the recognition cost. The proof is a one-line unfold: the ratio collapses to 1 and J(1)=0 finishes it.
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 $J(r/r)=J(1)=0$.
background
This sits in Physics RS Module 2, the structural certificate that the RS prediction for the inverse fine-structure constant lands in the open band $(137.030,137.039)$ (CODATA $137.036$ inside), marked RS_PASS with no sorry and no axioms.
The underlying cost is the Recognition Science J-functional. Upstream, $J(1)=0$ is recorded as the unit identity for that cost (equivalently $J(x)=(x-1)^2/(2x)$, or $\cosh(\log x)-1$). Domain cost is the local wrapper that feeds a pair of nonzero reals into $J$ of their ratio, so equal arguments are the pure unit case.
The module imports only Mathlib, Constants, and Cost, so the result is pure cost algebra, not yet the alpha arithmetic.
proof idea
One-line wrapper. Unfold the definition of domain cost so the goal is $J(r/r)=0$. Rewrite the ratio by div_self using $r\neq 0$, obtaining $J(1)=0$. Discharge by the upstream unit lemma Jcost_unit0.
why it matters
Gives the diagonal normalization every later cost comparison in the fine-structure module needs: self-matching scales carry zero recognition cost. That is the baseline against which nonzero domain defects (and the canonical threshold siblings) are measured when the module certifies the alpha band.
No downstream consumers are wired yet in the graph; the immediate siblings are nonnegativity of domain cost, positivity of the canonical threshold, and the module certificate RSPhysics002Cert. In the broader forcing chain this is ordinary J-cost hygiene under T5 (J-uniqueness), not a new forcing step. It closes no open scaffold; it is already a proved structural fact.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.