domainCost_at_eq
plain-language theorem explainer
For any nonzero real scale r, the materials domain cost of the self-pair (r,r) is exactly zero. Certificate and threshold arguments in the iron-melting materials module cite this to clear the on-diagonal term. The proof is a one-line wrapper: unfold the cost, reduce the ratio to 1, and apply the unit root of J.
Claim. For every real $r \neq 0$, the materials domain cost of the self-pair equals zero: evaluating the cost on $(r,r)$ yields $0$ (equivalently, $J(r/r) = J(1) = 0$).
background
Module 5 of the RS materials stack records the iron melting match $\phi^{15}\cdot\phi^{0.7},\mathrm{K}\approx 1814,\mathrm{K}$ against the experimental $1811,\mathrm{K}$ (0.2%), and packages the supporting identities as structural theorems with no sorry and no axioms.
The underlying cost is the T5 J-functional $J(x)=(x+x^{-1})/2-1$, equivalently $J(x)=(x-1)^2/(2x)$, uniquely fixed by the Recognition Composition Law. Its unit root is the lemma $J(1)=0$. Domain cost on a pair of real scales is the J-cost of their ratio, so self-comparison is the unit case.
Upstream, Jcost_unit0 states exactly $J(1)=0$ by unfolding the closed form of $J$.
proof idea
One-line wrapper. Unfold the definition of domain cost (which is $J$ of the ratio of the two arguments). Rewrite the self-ratio $r/r$ to $1$ by div_self using the hypothesis $r\neq 0$. Finish by the upstream unit lemma $J(1)=0$.
why it matters
Clears the diagonal of the materials domain cost so nonnegativity, threshold, and certificate lemmas in the same module can treat self-comparison as the zero baseline. The module status line marks the whole file as a structural theorem block (0 sorry, 0 axiom) supporting the iron-melting $\phi$-ladder match. In the broader forcing chain this rests on T5 J-uniqueness: once $J$ is fixed, $J(1)=0$ is forced, and every domain-cost identity inherits that root. No downstream consumers are wired yet in the graph; the lemma is local infrastructure for the materials certificate siblings (domainCost_nonneg, canonicalThreshold, RSMatl005Cert).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.