domainCost
plain-language theorem explainer
Domain cost assigns to a mass–energy pair the recognition cost of their ratio: J(m/e). It is the local building block for vacuum and threshold statements in the recognition-field vacuum module. Anyone citing nonnegativity of domain cost or the canonical threshold uses this abbreviation. The body is a one-line definition wrapping the unique J-cost functional.
Claim. For real $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 treats vacuum energy density in Recognition Science units as $\rho_{\mathrm{vac}}=J(\varphi)/\varphi^5$, with the RS vacuum identified as the ground state of the recognition field (all local $J=0$). The unique cost forced by the Recognition Composition Law is $J(x)=\frac12(x+x^{-1})-1$, also written $\cosh(\log x)-1$; it vanishes only at ratio one and is nonnegative for $x>0$.
Upstream, every import path exposes the same $J$-cost (Cost, Cosmology, Gravity bridges, Spiral). Domain cost simply specializes that functional to a mass-over-energy ratio, the natural dimensionless argument when comparing a mass scale to an energy scale inside the vacuum or threshold analysis.
proof idea
Pure definition: domainCost m e is definitionally Jcost (m / e). No lemmas or tactics; the equality is by rfl wherever needed downstream.
why it matters
Sits at the head of the Recognition Field Vacuum Energy Density development (Plan v7 structural pass). Sibling facts (domainCost_nonneg, domainCost_at_eq, canonicalThreshold) rest on this abbreviation, so the vacuum certificate and inhabited cert objects can speak in mass–energy language rather than raw ratios. Framework landmarks: T5 J-uniqueness and the RCL fix the shape of $J$; the vacuum formula $\rho_{\mathrm{vac}}=J(\varphi)/\varphi^5$ and the ground-state condition (all $J=0$) are the module’s target. No used-by edges are recorded yet; the def is infrastructure for those vacuum theorems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.