domainCost
plain-language theorem explainer
Domain cost of a real pair (m, e) is the recognition cost of their ratio m/e. Cosmology arguments that tie the scalar spectral index to J-cost use this as the local cost on mass-energy ratios. The body is a one-line definitional wrapper around the forced RS cost J.
Claim. For $m,e\in\mathbb{R}$, the domain cost is $J(m/e)$, where $J(x)=\frac{x+x^{-1}}{2}-1$ is the recognition cost of a positive ratio.
background
The module derives the scalar spectral index from the phi-ladder (Plan v7). Status is structural: zero sorry, zero axiom. Planck 2018 gives $n_s\approx 0.9649$; the RS inflation route yields $n_s=1-2/(N_e+1)=1-2/45=0.9556$, within about $3\sigma$.
The cost functional is the unique $J$ forced by the Recognition Composition Law (forcing chain T5): $J(x)=\frac12(x+x^{-1})-1$, also written $\cosh(\log x)-1$. Upstream copies state that a genuine distinction (ratio not one) has strictly positive cost, and that $J$ is nonnegative for positive arguments.
Here the cost is specialized to a mass-energy ratio: domain cost evaluates $J$ at $m/e$. Sibling lemmas in the same file record evaluation identities, nonnegativity, a canonical threshold, and the $n_s$ certificate built from that threshold.
proof idea
Definitional one-liner. No tactics and no lemmas: domainCost m e is definitionally Jcost (m / e), with Jcost the standard RS cost $(x+x^{-1})/2-1$ imported from Cost (and mirrored in several gravity and spiral modules).
why it matters
Places the forced J-cost (T5 / RCL uniqueness) into the cosmology spectral-index pipeline. The module goal is a structural account of $n_s$ from the phi-ladder and inflation counting ($N_e+1=45$), consistent with Planck within $3\sigma$.
Siblings domainCost_nonneg, canonicalThreshold, nS3Cert, and cert build the certificate stack on top of this abbreviation. Even with no external used_by edges recorded yet, the def is the cost interface those local certificates quantify over when they compare mass-energy ratios to the recognition threshold.
It does not itself compute $n_s$; it supplies the cost primitive those later steps need.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.