domainCost
plain-language theorem explainer
Domain cost assigns to a mass–energy pair the recognition cost of their ratio. Materials theorists cite it when packaging power-law creep (n = D = 3) in RS-native units. The body is a one-line alias of the unique J-cost on m/e.
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 measures mismatch by the J-cost $J(x)=\frac{x+x^{-1}}{2}-1$, forced by the Recognition Composition Law (T5). It vanishes only at ratio one and is nonnegative for $x>0$. Upstream modules (Cost, CoherenceCollapse, EnergyProcessingBridge) all expose the same functional.
This file is Materials RS Module 7: the creep exponent is fixed at $n=D=3$ as an exact structural claim (zero sorry, zero axiom). Domain cost is the local packaging of J on a mass-to-energy ratio, the natural dimensionless input for that materials setting.
proof idea
Pure definition: domainCost m e is definitionally Jcost (m / e). No tactics, no lemmas. Downstream nonnegativity and evaluation lemmas (siblings domainCost_nonneg, domainCost_at_eq) inherit directly from the corresponding facts about J.
why it matters
Gives the materials stack a named cost on mass/energy ratios so creep and threshold statements can stay in RS units without reopening the J-uniqueness argument. The module goal is the exact identification of the power-law creep exponent with spatial dimension three (T8: $D=3$; T7 eight-tick octave in the broader chain). No downstream theorems yet list this def as a dependency; siblings canonicalThreshold and the RSMatl007Cert certificate are the immediate consumers inside the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.