domainCost_at_eq
plain-language theorem explainer
Equal nonzero scale parameters incur zero domain cost under the J-cost functional. Cosmology and defect-network arguments cite this as the on-diagonal vanishing of the two-argument cost. The proof unfolds the definition, reduces the ratio to 1, and applies J(1)=0.
Claim. For every real $r \neq 0$, the two-argument domain cost satisfies $\mathrm{domainCost}(r,r)=0$.
background
The module builds a structural account of cosmic-string networks from the Recognition Science J-cost. In RS-native units the string tension scales as $G\mu = J(\varphi),(v/M_{\mathrm{Pl}})^2$, and the module records the numerical band against observational bounds $G\mu < 10^{-7}$.
The two-argument domain cost is the J-cost of the ratio of the two real scales: after unfolding, $\mathrm{domainCost}(r,s)$ is $J(r/s)$ (with $s\neq 0$). The cost functional itself is the unique nonnegative solution of the Recognition Composition Law fixed by the forcing chain (T5): $J(x)=(x+x^{-1})/2-1$, equivalently $J(x)=(x-1)^2/(2x)$, so $J(1)=0$.
Upstream, Jcost_unit0 states exactly that unit evaluation: $J(1)=0$.
proof idea
One-line wrapper. Unfold the definition of the two-argument domain cost, rewrite the ratio $r/r$ to $1$ by div_self (using $r\neq 0$), then apply the lemma $J(1)=0$.
why it matters
On-diagonal vanishing is the baseline sanity check for any cost used to weight domain or string configurations: matched scales carry no excess cost. In this module it sits beside nonnegativity and the canonical threshold that feed the cosmic-string certificate (CosmicStrings4Cert). The surrounding narrative ties the same $J$ to the RS string-tension formula $G\mu = J(\varphi),(E_{\mathrm{string}}/M_{\mathrm{Pl}})^2$ and the comparison with $G\mu < 10^{-7}$. No downstream dependents are recorded yet; the lemma is local infrastructure for the certificate and related nonnegativity facts.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.