domainCost
plain-language theorem explainer
Domain cost scores a mass-to-energy ratio by the recognition cost J(m/e). Cosmologists working the RS sound-horizon identity cite it when they need a dimensionless mismatch between two positive scales. The body is a one-line abbreviation of the forced J-cost on the quotient.
Claim. For real numbers $m$ and $e$, the domain cost is $J(m/e)$, where $J(x)=\frac{1}{2}(x+x^{-1})-1$ is the recognition cost of a positive ratio.
background
The module derives the CMB sound horizon $r_s\approx 147,\mathrm{Mpc}$ as an exact RS identity: $r_s=J(\varphi)\cdot\varphi^{14},\mathrm{Mpc}$. The surrounding development treats scale mismatches as arguments of the recognition cost rather than free parameters.
The cost functional is the unique $J$ forced by the Recognition Composition Law: $J(x)=\frac12(x+x^{-1})-1$ (equivalently $\cosh(\log x)-1$). Upstream modules (Cost, RefineTrigger, CoherenceCollapse, EnergyProcessingBridge) all expose the same $J$, with the standing fact that a genuine distinction ($x\neq 1$) has strictly positive cost and that $J\ge 0$ on positives.
Here $m$ and $e$ are two positive real scales (mass-like and energy-like in the local naming). Their ratio is the only invariant the cost sees; absolute units drop out.
proof idea
Pure definitional abbreviation: domainCost m e unfolds to Jcost (m / e). No lemmas, tactics, or side conditions are discharged at this site. Non-negativity and evaluation identities live in sibling lemmas (domainCost_nonneg, domainCost_at_eq).
why it matters
Gives the cosmology layer a named handle for the same $J$ that appears in the forcing chain (T5 J-uniqueness) and the RCL. The module status line is structural (0 sorry, 0 axiom) and pins $r_s=J(\varphi)\cdot\varphi^{14},\mathrm{Mpc}$ against the observed $147,\mathrm{Mpc}$ band. Downstream certificates in this file (SoundHorizon5Cert, canonicalThreshold) are the natural consumers; the present def is the shared cost primitive they evaluate. No used_by edges are recorded yet, so its role is local scaffolding for those certificates rather than a cross-module export.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.