domainCost
plain-language theorem explainer
Domain cost of a mass-energy pair is the recognition J-cost of their ratio m/e. Cosmologists building the BIT dark-energy kernel family cite it when placing equation-of-state drift in [0, J(φ)]. The body is a one-line specialization of the forced cost functional to that ratio.
Claim. For real $m$ and $e$, 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 builds BIT Kernel Family v3 from J-cost (Plan v7, structural, zero sorry). BIT dark-energy drift sits in $\delta w_0\in[0,J(\varphi)]$: pure $\Lambda$ at the lower end, maximum BIT drift $0.118$ at the upper end, with canonical kernel $K(z)=1/(1+z)$.
The upstream cost is the unique functional forced by the Recognition Composition Law: $J(x)=\frac12(x+x^{-1})-1$ (equivalently $\cosh(\log x)-1$). Upstream docs state it is the RS recognition cost of a positive ratio, nonnegative for $x>0$, and strictly positive off the identity ratio.
Here the two arguments are a mass-like scale $m$ and an energy-like scale $e$; their ratio is the natural dimensionless input to $J$.
proof idea
Pure definitional abbreviation: apply the global $J$-cost to the single ratio $m/e$. No lemmas, no tactics, no side conditions in the body.
why it matters
Gives the local cost scale that the BIT kernel family compares against the canonical threshold and the bound $J(\varphi)$. That bound is the T5 landmark: $J$ is the unique cost forced by RCL, and $\varphi$ is the T6 self-similar fixed point, so $J(\varphi)$ is the natural maximum drift amplitude quoted in the module header.
Sibling facts (equality at matched scales, nonnegativity, positive canonical threshold, and the BITKernel3 certificate) sit on top of this definition. Even with no recorded downstream edges yet, it is the cost primitive the v3 kernel certificates quantify against when they place $\delta w_0$ between pure $\Lambda$ and maximum BIT drift.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.