domainCost_at_eq
plain-language theorem explainer
Equal nonzero arguments make the domain cost vanish: the J-cost of a unit ratio is zero. Cosmology and ladder-normalization arguments cite this as the matched-scale baseline. Proof is a one-line unfold plus rewrite to 1, then the unit-zero lemma for J.
Claim. For every real $r \neq 0$, the domain cost of the matched pair $(r,r)$ is zero. Equivalently, if domain cost is $J$ of the scale ratio, then $J(r/r) = J(1) = 0$.
background
Module Cosmology.SoundHorizon5 treats the CMB sound horizon as a structural J-cost identity: $r_s = J(\varphi)\cdot\varphi^{14}$ Mpc, claimed exact at $147$ Mpc in RS units (with $\varphi^{14}\sim 843$ Mpc and $147/843\sim J(\varphi)$).
The Recognition cost is $J(x)=(x+x^{-1})/2-1$, also $J(x)=(x-1)^2/(2x)$ for $x>0$. Upstream lemma Jcost_unit0 records $J(1)=0$. Domain cost compares two real scales by feeding their ratio to $J$; equal arguments therefore reduce to the unit point of $J$.
Local setting is pure algebra on that cost: nonnegativity, thresholds, and the sound-horizon certificate sit beside this identity. No new physics is introduced here beyond the matched-scale normalization.
proof idea
One-line wrapper. Unfold domain cost to expose $J$ of the ratio $r/r$. Rewrite $r/r=1$ by div_self using $r\neq 0$. Finish with the upstream unit-zero lemma $J(1)=0$.
why it matters
Gives the zero baseline for domain comparisons in the sound-horizon development. The module is marked structural (0 sorry, 0 axiom) and aims at $r_s=J(\varphi)\cdot\varphi^{14}$ Mpc as an exact RS identity, tying the observed $\sim 147$ Mpc scale to T5 J-uniqueness and the phi-ladder.
No recorded downstream dependents yet; siblings cover nonnegativity, a canonical threshold, and the certificate inhabitation. The lemma is the algebraic sanity check that a perfectly matched pair carries no excess cost before thresholds or rung gaps are applied.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.