domainCost
plain-language theorem explainer
Domain cost of a materials pair (m, e) is the recognition cost J of the ratio m/e. Materials workers matching steel Young's modulus to the phi-ladder cite it as the local cost on modulus-like ratios. It is a one-line definitional wrapper around the unique J forced by the Recognition Composition Law.
Claim. For real numbers $m$ and $e$, the domain cost is $J(m/e)$, where $J(x)=\frac{x+x^{-1}}{2}-1$.
background
Recognition Science measures mismatch of positive ratios by the unique cost $J(x)=\frac{x+x^{-1}}{2}-1$ (equivalently $\cosh(\log x)-1$). Upstream docs state it is "the unique cost functional forced by the Recognition Composition Law" and that "a genuine distinction (ratio not one) has strictly positive cost." It is nonnegative for $x>0$ and vanishes only at $x=1$.
This module (Materials RS Module 1) is a structural theorem package (0 sorry, 0 axiom) aimed at the steel Young's modulus match: $\varphi^{25},\mathrm{MPa}\approx 196,\mathrm{GPa}$, near the experimental $\sim 200,\mathrm{GPa}$. Domain cost is the materials-side specialization of $J$ to a pair of reals interpreted as a modulus-like ratio $m/e$.
proof idea
Definitional one-liner: the value is exactly $J(m/e)$ by unfolding. No tactics, no lemmas, no proof obligations beyond the ambient definition of $J$.
why it matters
Gives the materials module a single named cost on pairs so sibling facts (value at equality, nonnegativity) and the certificate RSMatl001Cert can talk about threshold crossings without re-inlining $J$. It reuses the same $J$ already fixed at T5 in the forcing chain and imported across cosmology, gravity, and spiral modules, keeping the steel $\varphi^{25}$ match on the same cost geometry as the rest of RS. No downstream theorems are wired yet; the immediate consumers are the in-module nonnegativity and threshold lemmas that support the structural modulus claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.