domainCost
plain-language theorem explainer
Domain cost assigns to a materials pair (m, e) the recognition cost of their ratio m/e. Materials workers in the Mohs-scale diamond module use it as the local cost functional on mass-energy ratios. The declaration is a one-line abbreviation of the forced J-cost at 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
Materials RS Module 4 is a structural (zero-sorry) fragment tying the Mohs hardness of diamond to the RS constant $\varphi^5\approx 11.09$, read as order-10 on the Mohs scale. The module imports the global cost layer and constants.
The upstream object is the J-cost $J(x)=\frac{1}{2}(x+x^{-1})-1$, documented across Cost and related modules as the recognition cost of a positive ratio and as the unique cost forced by the Recognition Composition Law. A genuine distinction (ratio not one) has strictly positive cost; $J$ is nonnegative on positives.
Domain cost simply specializes that functional to a materials mass-to-energy (or analogous scale) ratio $m/e$, so later lemmas can talk about thresholds and nonnegativity in materials language without reopening the definition of $J$.
proof idea
Definitional abbreviation only: expand domainCost m e to Jcost (m / e). No tactics, no lemmas, no side conditions at the definition site. Downstream facts (equality at one, nonnegativity) are separate theorems on this def.
why it matters
Gives the materials module a named cost on ratios so the diamond/Mohs structural story can sit on the same J that the forcing chain isolates at T5 (J-uniqueness from the Recognition Composition Law). Sibling results in the same file (domainCost_at_eq, domainCost_nonneg, canonicalThreshold, and the module certificate) are the immediate consumers; the page lists no external used_by edges yet.
The module framing is structural: $\varphi^5\in(11,12)$ as the RS-native stand-in for Mohs 10. Domain cost is the cost primitive those comparisons rest on, not the Mohs identification itself. It keeps materials statements aligned with the global cost calculus rather than inventing a parallel functional.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.