domainCost
plain-language theorem explainer
Domain cost assigns to a mass-energy pair the recognition cost of their ratio: J(m/e). Structural Standard Model arguments in the eight-tick module use it as the scalar cost of placing a mass against an energy scale. The body is a one-line specialization of the unique J-cost functional.
Claim. For real $m$ and $e$, the domain cost is $J(m/e)$, where $J(x)=\frac{x+x^{-1}}{2}-1$ is the recognition cost of a positive ratio.
background
The ambient module is Standard Model RS Structural Module 5. Its setting is the RS eight-tick: one full traversal of the binary recognition lattice with period $2^D=8$ (forcing-chain landmark T7). Status is structural: zero sorry, zero axiom.
The cost functional is the unique J forced by the Recognition Composition Law (T5): $J(x)=\frac{1}{2}(x+x^{-1})-1$, also written $\cosh(\log x)-1$. Upstream docs state it is the RS recognition cost of a positive ratio, nonnegative for $x>0$, and strictly positive when the ratio is not one. Domain cost simply feeds the mass-to-energy ratio into that functional.
proof idea
Pure definition, no proof obligations. The body applies the shared noncomputable J-cost to the quotient $m/e$. No lemmas are invoked; downstream nonnegativity and threshold facts are separate sibling declarations.
why it matters
Gives the Standard Model structural layer a named scalar for how costly a mass is relative to an energy scale under the forced J. It sits next to sibling facts (evaluation identity, nonnegativity, canonical threshold positivity) and the module certificate RSSTDStructural005Cert. Framework landmarks in play are T5 J-uniqueness and T7 eight-tick octave. No downstream used_by edges are recorded yet; the def is infrastructure for those structural claims rather than a terminal theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.