domainCost
plain-language theorem explainer
Domain cost of a mass-energy pair is the recognition cost of their ratio m/e. Foundation and threshold arguments in the eight-tick structural module cite it as the local cost measure. It is a one-line definition that applies the unique J-cost functional to that ratio.
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
Recognition Science forces a unique cost on positive ratios: $J(x)=\frac{x+x^{-1}}{2}-1$, equivalently $\cosh(\log x)-1$. Upstream modules record the same functional (often written $\tfrac12(x+x^{-1})-1$) and note it is the unique solution of the Recognition Composition Law; genuine distinctions ($x\neq 1$) carry strictly positive cost, and $J$ is nonnegative on positives.
This module is Foundation structural item 5: the RS eight-tick, period $2^D=8$, one full traversal of the binary recognition lattice, status structural (0 sorry, 0 axiom). Domain cost specializes $J$ to a mass-over-energy ratio, the natural dimensionless argument when comparing a mass scale to an energy (or frequency) scale inside that lattice.
proof idea
Pure definition: evaluate the shared $J$-cost functional at the ratio $m/e$. No lemmas, tactics, or side conditions; the body is the single application $J(m/e)$.
why it matters
Gives the structural module a named cost on mass-energy pairs so later certificates can talk about thresholds without reopening the form of $J$. Sibling results (equality at a point, nonnegativity, the canonical threshold and its positivity, and the RS-FDN-Structural-005 certificate) sit on top of this abbreviation. Framework landmarks: T5 $J$-uniqueness and the RCL fix the functional being applied; T7 (eight-tick octave, period $2^3$) and T8 ($D=3$) fix the lattice setting of the module. No downstream uses are recorded yet; the definition is local scaffolding for the certificate bundle in this file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.