domainCost
plain-language theorem explainer
Defines the materials-domain recognition cost of a mass-to-energy ratio as the standard J-cost of m/e. Materials proofs that compare thermal or mass scales to energy scales cite this wrapper. The body is a one-line abbreviation of Jcost.
Claim. For real $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 ratios by the unique cost $J(x) = \frac{1}{2}(x + x^{-1}) - 1$, forced by the Recognition Composition Law (T5). Upstream modules record the same functional: "the RS recognition cost of a positive ratio" and "the unique cost functional forced by the Recognition Composition Law."
This file is Materials RS Module 6, a structural (zero-sorry) treatment of water's specific heat: $\phi^{19}\cdot 0.447,\mathrm{J/kg/K} = 4179,\mathrm{J/kg/K}$ matching $4179.6$ to $0.01%$. Domain cost supplies the local cost of a mass-versus-energy ratio before thresholds and certificates are stated.
Sibling lemmas immediately specialize the definition (evaluation at equality, non-negativity) and introduce a canonical positive threshold used by the module certificate.
proof idea
Pure definitional abbreviation: domainCost m e is definitionally Jcost (m / e). No tactics or lemmas; downstream facts unfold this equality and inherit non-negativity and uniqueness properties of $J$.
why it matters
Gives the materials layer a named cost of mass-to-energy imbalance in the same $J$ language used across cosmology, gravity, and spiral modules. That keeps Module 6's water $c_p$ structural theorem aligned with the forced T5 cost rather than an ad-hoc materials functional. Downstream siblings (domainCost_nonneg, canonicalThreshold, RSMatl006Cert) build the non-negativity and certificate stack on this wrapper; the used-by list is currently empty at the global edge level, so the immediate consumers are in-module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.