domainCost
plain-language theorem explainer
Domain cost scores a pair of real scales by the recognition cost of their ratio: J(m/e). Standard-model structural arguments cite it whenever a mass or energy ratio must be measured in the unique RS cost functional. The definition is a one-line specialization of Jcost to the quotient m/e.
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 scales by the J-cost $J(x) = \frac{1}{2}(x + x^{-1}) - 1$. Upstream modules record the same functional: it is the unique cost forced by the Recognition Composition Law, vanishes only at ratio one, and is nonnegative for $x > 0$.
This module is StandardModel structural module 6, whose stated theme is RS phi uniqueness (the self-similar fixed point $\varphi = 1 + 1/(1+1/(1+\cdots))$), status structural theorem with zero sorry and zero axiom. Domain cost is the local wrapper that feeds mass or energy ratios into that cost.
proof idea
Pure definition: apply the imported J-cost to the quotient $m/e$. No lemmas, no tactics; the body is the single term $Jcost(m/e)$.
why it matters
Gives the Standard Model layer a named handle on ratio cost so later structural facts (nonnegativity, evaluation at equality, canonical thresholds in the same file) can speak about mass or energy pairs without reopening the definition of $J$. It sits under the T5 J-uniqueness landmark and the RCL-forced cost, and supports the module's phi-uniqueness narrative by measuring how far a scale pair sits from self-similar balance. No downstream uses are recorded yet; siblings such as nonnegativity and the structural certificate are the immediate consumers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.