domainCost

The module treats the CMB damping multipole as an RS structural claim: $\ell_D$ sits between $\phi^{15}\approx 1364$ and $\phi^{16}\approx 2207$, matching the observed $1500$–$2000$ band. Status is a structural theorem package with no sorry and no axioms.

The cost functional is the unique $J$ forced by the Recognition Composition Law (T5): $J(x)=\frac{x+x^{-1}}{2}-1$, also written $\cosh(\log x)-1$. Upstream copies of Jcost state the same formula and record that a genuine distinction (ratio not one) has strictly positive cost, and that $J$ is nonnegative for positive arguments.

Here $m$ and $e$ are treated as real scales whose ratio is fed to $J$. The definition does not itself enforce positivity of the arguments; that is left to callers and to sibling lemmas.

Pure definition: apply the standard recognition cost $J$ to the single ratio $m/e$. No tactics, no lemmas, no hypotheses. Downstream equalities and nonnegativity are proved separately (siblings such as the pointwise equality and nonnegativity facts).

Gives the local cost language for the CMB damping-scale v3 certificate. In RS, physical thresholds are read off the phi-ladder; comparing a mass-like scale to an energy-like scale through $J(m/e)$ is the natural cost of that distinction. The module places $\ell_D$ between $\phi^{15}$ and $\phi^{16}$, consistent with the observed damping multipole band. This definition is the cost primitive those comparisons sit on, tying cosmology numerics back to the forced $J$ of the T5 uniqueness step and the RCL. No downstream used-by edges are recorded yet; siblings build the certificate and threshold facts around it.