domainCost_at_eq
plain-language theorem explainer
Equal nonzero domain scales carry zero recognition cost: the cost of the pair (r,r) vanishes. Horizon-problem and inflation-certificate arguments in RS cosmology cite this as the zero-defect baseline on a single causal domain. The proof unfolds the cost, reduces the ratio to 1, and applies the unit root of J.
Claim. For every real $r \neq 0$, the domain cost of the equal pair vanishes: the J-cost of the scale ratio $r/r$ is zero.
background
The ambient module treats the cosmological horizon problem as a structural consequence of the eight-tick forcing chain and the J-cost. Status is a structural theorem (no sorry, no axioms): inflation supplies $N_e = 44$ e-folds at temperature $T = J(\varphi),T_{\mathrm{Planck}}$, with $\varphi^{44}$ giving the RS expansion factor.
Domain cost compares two positive scale parameters by feeding their ratio into the recognition cost $J$. Upstream, $J$ is normalized so that $J(1) = 0$ (lemma Jcost_unit0), equivalently $J(x) = (x-1)^2/(2x)$. Thus any equal pair of nonzero scales is a pure unit ratio and must sit at the global minimum of $J$.
This zero identity is the baseline against which nonzero domain mismatches (and the canonical threshold used later in the same file) are measured.
proof idea
One-line wrapper. Unfold the definition of domain cost (ratio of the two arguments into $J$), rewrite $r/r = 1$ by the nonzero hypothesis, and finish with the upstream unit root $J(1) = 0$.
why it matters
Places the zero of domain cost on the same footing as the unit root of $J$, which is forced already at T5 of the unified forcing chain ($J(x) = (x+x^{-1})/2-1$). In the horizon-problem module this identity anchors the claim that a single causal domain after $\varphi^{44}$ expansion carries no residual recognition defect, consistent with the structural resolution sketched in the module doc (inflation at $T = J(\varphi),T_{\mathrm{Planck}}$).
No downstream dependents are recorded yet; sibling lemmas (nonnegativity of domain cost, positivity of the canonical threshold, and the inhabited horizon-problem certificate) sit beside it and will consume the zero baseline when the certificate is assembled. It does not itself prove the e-fold count or the $10^{24}$--$10^{26}$ causal-contact bound; those live in the surrounding certificate construction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.