domainCost
plain-language theorem explainer
The domain cost of a mass-energy pair is the recognition cost of their ratio: J(m/e). Structural work on the eight-tick lattice cites this as the standard scalar that measures how far a mass sits from an energy scale. 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
Recognition Science measures mismatch of positive ratios by the J-cost $J(x) = \frac12(x + x^{-1}) - 1$, equivalently $\cosh(\log x) - 1$. Upstream modules record that this functional is the unique cost forced by the Recognition Composition Law (T5 in the forcing chain), and that $J(x) \ge 0$ for $x > 0$ with equality only at $x = 1$.
This module is Mathematics RS Structural Module 5: the eight-tick octave (period $2^D = 8$), one complete traversal of the binary recognition lattice. Domain cost simply feeds a mass-to-energy ratio into $J$, so that later lemmas can talk about nonnegativity and thresholds without reopening the definition of $J$.
proof idea
Pure definitional abbreviation: apply the existing J-cost functional to the quotient $m/e$. No lemmas or tactics; the body is the term $J(m/e)$.
why it matters
Gives the structural module a named scalar for how far a mass sits from a chosen energy scale on the recognition lattice. Sibling results (nonnegativity of domain cost, equality cases, canonical threshold positivity, and the module certificate) build directly on this abbreviation. In the broader framework it is the local instance of T5 J-uniqueness applied to mass/energy ratios inside the eight-tick (T7) setting; it does not itself force $\phi$, $D=3$, or the mass ladder, but supplies the cost language those later steps use.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.