domainCost
plain-language theorem explainer
Domain cost assigns to a mass-energy pair the recognition cost of their ratio. Structural and threshold arguments in the RS mathematics module cite it as the local cost on (m,e). It is a one-line definition: apply the unique J-cost functional 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
Recognition Science forces a unique nonnegative cost on positive ratios: $J(x)=\frac12(x+x^{-1})-1$, equivalently $\cosh(\log x)-1$. Upstream modules record the same functional as the cost forced by the Recognition Composition Law (T5 in the forcing chain).
This module packages structural RS predictions: that $J$ form, $\varphi$ as the self-similar fixed point, and $D=3$. Domain cost specializes $J$ to a mass-energy ratio $m/e$, the natural dimensionless input when comparing a mass scale to an energy scale in the same units.
Sibling lemmas then treat nonnegativity at equality cases and a canonical threshold built from this cost; the definition itself only names the composite.
proof idea
Pure definitional wrapper. The body is the application of the shared $J$-cost functional to the quotient $m/e$. No tactics, no lemmas, no side conditions in the type.
why it matters
Gives the mathematics module a named mass-energy cost so later structural claims (nonnegativity, equality at $m=e$, canonical threshold positivity, and the inhabited certificate for RS_MTH_Structural_001) can quote a single symbol rather than inline $J(m/e)$.
It sits on the T5 landmark: uniqueness of $J$ under the Recognition Composition Law. The module status line marks the package as a structural theorem block with zero sorry and zero axiom; this def is the cost primitive those theorems consume.
No external used-by edges are recorded yet; value is local to the structural certificate and its sibling lemmas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.