domainCost
plain-language theorem explainer
Defines the domain cost of a mass-to-energy ratio as the J-cost of m/e. Anyone working the recognition spectrum or phi-ladder energy levels cites this as the local cost functional on (m,e). It is a one-line abbreviation of the unique RS cost J.
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 builds the recognition spectrum of $H_{RS}$ on the phi-ladder: levels $E_n = J(\varphi^n),\hbar_R,\omega_0$ for $n = 0,1,2,\ldots$, with ground state $E_0 = 0$ and first excited state the recognition quantum $E_1 = J(\varphi),\hbar_R,\omega_0$.
The cost functional $J$ is the unique nonnegative function forced by the Recognition Composition Law: $J(x) = \frac{x + x^{-1}}{2} - 1$ (equivalently $\cosh(\log x) - 1$). It vanishes only at ratio one and is strictly positive for any genuine distinction. Upstream modules (Cost, CoherenceCollapse, EnergyProcessingBridge, SpiralField) all use this same $J$.
Here the arguments are a mass-like scale $m$ and an energy-like scale $e$; their ratio is the dimensionless input to $J$.
proof idea
Pure definitional abbreviation: domain cost of $(m,e)$ is exactly $J(m/e)$. No proof obligations; the body is the single application of the shared $Jcost$ definition.
why it matters
Gives the module a named cost on mass-energy pairs so later spectrum certificates (canonical threshold, nonnegativity, RecogSpectrum3Cert) can speak in domain language rather than raw $J$. Ties directly to T5 J-uniqueness in the forcing chain and to the RCL-forced cost that underwrites the phi-ladder mass formula and the recognition quantum. Even with no recorded downstream edges yet, the sibling lemmas (domainCost_nonneg, domainCost_at_eq, canonicalThreshold) sit on top of this def.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.