domainCost

The module treats Penrose-process efficiency as a structural consequence of the recognition cost: $\eta_{\mathrm{Penrose}}=J(\varphi),(\Omega_H/\Omega_{\mathrm{ISCO}})$, giving $\sim 19.1%$ at maximal Kerr against an empirical ceiling near $20.7%$.

The cost functional is the unique $J$ forced by the Recognition Composition Law, $J(x)=\frac12(x+x^{-1})-1$ (equivalently $\cosh(\log x)-1$). Upstream modules restate the same $J$ as the RS recognition cost of a positive ratio, nonnegative for $x>0$, and strictly positive off the identity ratio.

Here $m$ and $e$ are treated as a mass and an energy scale whose ratio is fed to $J$; the definition packages that evaluation as a named domain cost for later threshold and certificate lemmas in the same file.

Pure definitional abbreviation: domainCost m e is definitionally Jcost (m / e). No tactics, no lemmas, no side conditions in the body. Downstream nonnegativity or evaluation lemmas (siblings such as domainCost_nonneg, domainCost_at_eq) discharge positivity or specialize the ratio.

Gives the gravity module a single name for “J-cost of the mass-to-energy ratio,” which is the natural input to Penrose-efficiency bookkeeping built from $J(\varphi)$ and horizon/ISCO angular velocities. It sits under the T5 uniqueness of $J$ and the RCL-forced cost, so efficiency statements inherit the same functional rather than an ad hoc loss. Sibling certificates (PenroseProcess3Cert, canonicalThreshold) are the intended consumers; the present declaration itself has no further used_by edges yet. It does not close the empirical $20.7%$ comparison; it only supplies the cost map those comparisons compose.