domainCost_at_eq
plain-language theorem explainer
The Recognition domain cost vanishes on the diagonal: comparing any nonzero real scale to itself yields cost zero. Physicists tracking ratio costs in the Weinberg-angle module cite this identity as the baseline calibration. Proof is a one-line wrapper: unfold the cost, reduce the ratio to 1, apply J(1)=0.
Claim. For every real $r \neq 0$, the domain cost of $r$ against itself is zero. Equivalently, if the cost is the $J$-functional of the ratio of the two arguments, then $J(r/r) = J(1) = 0$.
background
Physics RS Module 4 packages structural identities around the tree-level Weinberg angle $\sin^2\theta_W = J(\varphi)/(1+J(\varphi)) \approx 0.1054$ (loop-corrected toward $0.231$). The module works in RS-native units with the standard cost $J$, also written $J(x)=(x-1)^2/(2x)$.
The local domainCost is the $J$-cost of a ratio of two real scales. Its natural calibration is that a scale compared to itself must cost nothing. That fact is supplied upstream by Jcost_unit0: $J(1)=0$, obtained by direct simplification of the closed form of $J$.
proof idea
One-line wrapper. Unfold the definition of domain cost (which is $J$ of the ratio of its two arguments). Rewrite $r/r=1$ by the standard division identity under the hypothesis $r\neq 0$. Finish by applying the upstream lemma $J(1)=0$.
why it matters
Diagonal vanishing is the zero-point of every ratio cost used later in the module (nonnegativity of domain cost, the canonical threshold, and the RSPhysics004 certificate that packages the Weinberg structural claim). It is the cost-side counterpart of T5 $J$-uniqueness: $J$ is normalized so the self-ratio is the unique zero of the cost on the positive reals. No downstream theorems currently depend on this declaration by name; it sits as a local calibration lemma inside the module's certificate stack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.