domainCost
plain-language theorem explainer
Domain cost assigns the Recognition Science J-cost to the dimensionless ratio of a mass parameter to an energy scale. Materials theorists working the Hall-resistance structural line cite it as the local cost of a mass–energy mismatch. The body is a one-line abbreviation of the unique cost functional J.
Claim. For real parameters $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
Module 8 of the Materials strand is a structural package whose headline is the Hall resistance $R_H=h/e^2$ recovered from the RS fine-structure derivation. Status is structural theorem: zero sorry, zero axiom.
The only primitive used here is the recognition cost $J$. Across Cost, Cosmology, Gravity, and Spiral it is defined by $J(x)=\frac12(x+x^{-1})-1$. Upstream docs state that this is the unique cost forced by the Recognition Composition Law, that a genuine distinction (ratio not one) has strictly positive cost, and that $J$ is nonnegative for positive arguments.
Domain cost simply feeds the mass-to-energy ratio into that functional, giving a scalar mismatch cost native to the materials setting.
proof idea
Pure definitional abbreviation: apply the shared $J$-cost functional to the quotient $m/e$. No tactics, no lemmas, no hypotheses.
why it matters
Gives the materials module a named cost of mass–energy mismatch built from the same $J$ forced at T5 of the unified forcing chain (and uniquely characterized by the Recognition Composition Law). Sibling lemmas immediately record evaluation at equality and nonnegativity; the module certificate RSMatl008Cert packages the structural Hall-resistance claim. No downstream consumers are wired yet in the graph, so the definition is presently a local building block rather than a bridge lemma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.