domainCost_at_eq
plain-language theorem explainer
Equal nonzero scales incur zero domain cost: the J-cost of the ratio r/r vanishes. Cited as the diagonal normalization in RS Physics Module 6 (Higgs VEV vs Z-mass scale comparisons). One-line wrapper: unfold, cancel the ratio, apply J(1)=0.
Claim. For every real $r\neq 0$, the domain cost of matching the scale $r$ against itself is zero.
background
Recognition Science measures scale mismatch by the J-cost $J(x)=(x+x^{-1})/2-1$, also written $(x-1)^2/(2x)$. The elementary root is $J(1)=0$ (lemma Jcost_unit0).
This module (RS Physics Module 6) treats the Higgs vacuum expectation relative to the $Z$ mass: $v/M_Z\approx 2.70$ versus $\varphi^2\approx 2.618$ (about 3% off). Domain cost is the J-cost of the ratio of its two real arguments, so the diagonal case is exactly $J(1)$.
The local setting is a structural physics certificate: zero sorry, zero axioms, built on the Cost and Constants imports.
proof idea
One-line wrapper. Unfold the definition of domain cost (ratio of the two arguments fed to $J$). Rewrite $r/r=1$ by division-by-self under $r\neq 0$. Finish with the upstream lemma that $J(1)=0$.
why it matters
Supplies the zero baseline for domain cost on equal scales, the natural normalization before any off-diagonal comparison of the Higgs VEV ratio to $\varphi^2$. Sits with sibling facts (nonnegativity, canonical threshold positivity) that feed the Module 6 certificate. No recorded downstream dependents yet; it is infrastructure for the structural Higgs-scale claim rather than a forcing-chain step (T5--T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.