domainCost
plain-language theorem explainer
Domain cost scores a mass-to-energy ratio by the unique RS cost functional J. Anyone building the recognition Hilbert space H_RS or a mass/energy threshold cites it as the local cost on the recognition manifold. The body is a one-line abbreviation: apply J to m/e.
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 constructs the recognition Hilbert space $H_{RS}=L^2$ on the recognition manifold, with basis labels $|n,\sigma,Z,\Theta\rangle$ (rung, spin-like, charge-like, and phase coordinates) and Hamiltonian built from weighted number operators with weights $J(\phi^k)$.
The cost functional $J$ is the unique nonnegative functional forced by the Recognition Composition Law: $J(x)=\frac12(x+x^{-1})-1$ for $x>0$ (equivalently $\cosh(\log x)-1$). Upstream definitions across Cost, Cosmology, Gravity, and Spiral all pin the same formula and the fact that a genuine distinction (ratio not one) has strictly positive cost.
Here $m$ and $e$ are treated as real scalars; the interesting regime is positive $e$ so that the ratio $m/e$ is the dimensionless argument of $J$.
proof idea
Pure definitional abbreviation. No tactics or lemmas: domainCost m e is definitionally Jcost (m / e), with Jcost the shared RS cost $J(x)=\frac12(x+x^{-1})-1$.
why it matters
Gives the local scalar cost that later certificates and thresholds in this module (nonnegativity of domain cost, canonical threshold positivity, and the RecogHilbert3Cert package) can quote without reopening the J formula. It sits under the T5 landmark: J-uniqueness from the forcing chain, so every mass/energy comparison in $H_{RS}$ inherits the same cost that appears in the Hamiltonian weights $J(\phi^k)$ and in the RCL identity. No downstream edges are recorded yet; the immediate consumers are the sibling lemmas that prove nonnegativity and fix the canonical threshold on this cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.