domainCost
plain-language theorem explainer
The domain cost of a mass-energy pair is the recognition cost of their ratio: J(m/e). Gravity and Planck-star arguments cite it as the scalar that measures how far a configuration sits from the balanced ratio m = e. The definition is a one-line specialization of the unique J-cost forced by the Recognition Composition Law.
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 develops the Planck-star bounce on the phi-ladder: a black-hole interior reaches a minimum radius $r_{\min} = \phi^{N/2},\ell_{\mathrm{Pl}}$ with bounce density $\rho_{\mathrm{bounce}} = \rho_{\mathrm{Pl}},\phi^{-3N/2}$. The structural claim is zero-sorry and axiom-free.
The only primitive cost is the J-functional $J(x) = \frac12(x + x^{-1}) - 1$, forced uniquely by the Recognition Composition Law (T5). Upstream modules record the same formula and the elementary facts that $J(x)\ge 0$ for $x>0$ and $J(x)=0$ precisely at $x=1$. Domain cost simply feeds the mass-to-energy ratio into that functional, so a balanced pair $(m,e)$ with $m=e$ has vanishing cost and any genuine mismatch is strictly positive.
proof idea
Pure definitional abbreviation: domainCost m e is defined to be Jcost (m / e). No lemmas are applied; the body is the single application of the shared J-cost to the ratio of the two real arguments.
why it matters
Inside the Planck-star development this scalar is the natural cost of a mass-energy domain before thresholds and certificates are stated. Sibling results (non-negativity, evaluation identities, the canonical threshold, and the PlanckStar3Cert package) build directly on it. Framework-wise it is the gravity-side instance of the T5 J-uniqueness landmark: the same cost that appears in the forcing chain and the RCL is reused without modification to score how far a stellar or collapse configuration sits from balance. It therefore ties the bounce-density scaling $\phi^{-3N/2}$ back to the unique recognition cost rather than an ad-hoc potential.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.