domainCost_at_eq
plain-language theorem explainer
The domain cost of any diagonal pair (r,r) with r nonzero is zero. Cosmology arguments that normalize a reference multipole or ladder rung to unit ratio cite this identity before scoring peak spacings. The proof unfolds the cost to J of a ratio, reduces r/r to 1, and applies the unit-zero lemma for J.
Claim. For every real $r\neq 0$, the domain cost of the diagonal pair $(r,r)$ vanishes: the J-cost of the ratio $r/r$ equals $0$.
background
This module records structural theorems for CMB acoustic peak locations in Recognition Science. Observed multipoles $l_1\sim 220$, $l_2\sim 540$, $l_3\sim 800$ are compared to pure $\varphi$-power ratios ($l_2/l_1\approx\varphi^2$, $l_3/l_1\approx\varphi^{2.8}$).
Domain cost is the J-cost of the ratio of two nonzero real scales. The cost $J$ is the unique nonnegative functional forced by the Recognition Composition Law; equivalently $J(x)=(x+x^{-1})/2-1$, with base value $J(1)=0$.
Upstream, Jcost_unit0 states exactly that unit evaluation: $J(1)=0$. Any diagonal domain-cost claim reduces to that fact once the ratio is rewritten to 1.
proof idea
One-line wrapper. Unfold domain cost (J of the argument ratio), rewrite $r/r=1$ by div_self using $r\neq 0$, then apply the upstream lemma $J(1)=0$.
why it matters
Local normalization lemma for the CMB peak stack in this module (siblings include nonnegativity of domain cost, the canonical threshold, and the v3 peak-position certificate). Diagonal vanishing removes an additive offset so that multipole ratios can be scored purely against $\varphi$-powers.
In the broader framework this is the T5 base case of J: cost measures departure from the self-similar fixed point forced at T6. The module claims CMB peak spacing tracks those powers; the identity is the zero of that score. No downstream edges are recorded yet; the result is internal scaffolding for the structural cert.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.