domainCost
plain-language theorem explainer
The domain cost of a mass–energy pair is the recognition cost of their ratio. Anyone working the neutron-lifetime or mass-ladder side of RS cites it as the local cost functional on (m,e). It is a one-line definition that feeds m/e into the standard J-cost.
Claim. For real numbers $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 of positive ratios by the J-cost $J(x)=\frac{x+x^{-1}}{2}-1$, equivalently $\cosh(\log x)-1$. Upstream, this is the unique cost forced by the Recognition Composition Law (T5 in the forcing chain): any genuine distinction (ratio not one) has strictly positive cost, and $J$ is nonnegative on positives.
This module (Physics RS Module 3) is a structural certificate for the neutron lifetime identity $\phi^{17}\cdot 0.246,\mathrm{s}=878.5,\mathrm{s}$ against the PDG value $878.4,\mathrm{s}$. Domain cost supplies the local cost of a mass-to-energy ratio inside that physics layer, before thresholds and nonnegativity lemmas are applied.
proof idea
Pure definitional abbreviation: apply the imported J-cost functional to the ratio $m/e$. No proof obligations; the body is exactly $J(m/e)$.
why it matters
Gives the module a named cost on mass–energy pairs so later lemmas (nonnegativity, evaluation at equality, canonical threshold) can speak about domain cost rather than raw $J$. It sits under the T5 J-uniqueness landmark and the RS mass/energy bookkeeping used for the neutron-lifetime pass. Downstream siblings in the same file build the certificate RSPhysics003Cert on top of this cost; the declaration itself has no external used-by edges yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.