domainCost_at_eq
plain-language theorem explainer
For any nonzero real scale r, the domain cost of matching r against itself is exactly zero. Cosmology certificates that normalize ratios to a reference scale cite this diagonal identity. The argument unfolds the cost, cancels the self-ratio to 1, and applies the unit root of the J-cost.
Claim. For every real $r \neq 0$, the recognition domain cost of the pair $(r,r)$ vanishes: the J-cost of the self-ratio $r/r$ equals $0$.
background
Module RS_Cosmo_Module_012 packages structural facts for the Li-7 Spite plateau in Recognition Science cosmology. Observed lithium abundance sits in $(4.0,5.2)\times 10^{-10}$; the RS band is $(4.69,4.86)\times 10^{-10}$, marked RS_PASS with no sorry and no axioms.
The underlying cost is the J-functional from the forcing chain (T5): $J(x)=(x-1)^2/(2x)$, equivalently $\cosh(\log x)-1$. Upstream lemma Jcost_unit0 records the normalization $J(1)=0$. Domain cost compares two real scales by feeding their ratio into $J$; the present identity is the diagonal case of that definition.
proof idea
One-line wrapper. Unfold the domain-cost definition (ratio into $J$), rewrite $r/r=1$ by div_self using $r\neq 0$, then apply Jcost_unit0 which states $J(1)=0$.
why it matters
Keeps the cosmology cost calculus normalized: zero self-mismatch is the baseline against which off-diagonal domain costs and canonical thresholds are measured. Siblings in the same module (domainCost_nonneg, canonicalThreshold_pos, the RSCosmo012Cert bundle) rely on a well-behaved cost that vanishes on equal scales. In the broader framework this is the unit root of the T5 J-cost, the same functional fixed by the Recognition Composition Law. No downstream consumers are wired yet; the lemma is local scaffolding for the Li-7 structural certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.