domainCost
plain-language theorem explainer
Defines the domain cost of a mass-to-energy ratio as the recognition cost J(m/e). Falsifiability certificates and threshold lemmas in this module cite it as the scalar that must stay inside the RS band. The body is a one-line abbreviation of the forced J-cost on the ratio.
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 forces a unique nonnegative cost on positive ratios: $J(x)=\frac{1}{2}(x+x^{-1})-1$, equivalently $\cosh(\log x)-1$. Upstream modules record the same functional (T5 J-uniqueness) and note that any genuine distinction ($x\neq 1$) has strictly positive cost. The Recognition Composition Law fixes this $J$ uniquely among admissible costs.
This module packages structural falsifiability for RS: a measurement outside the predicted band at $3\sigma$ defeats the framework. Named external falsifiers include $\Lambda$ outside $(1.88,2.03)$, $\alpha^{-1}$ outside $(137.030,137.039)$, and BTFR slope outside $(3.8,4.2)$. Domain cost supplies the scalar comparison of a mass-like quantity $m$ against an energy-like scale $e$ inside that certificate stack.
proof idea
Pure definitional abbreviation: apply the standard $J$-cost to the ratio $m/e$. No lemmas, no tactics, no hypotheses.
why it matters
Gives the module a single named scalar for "how far is this mass/energy pair from recognition equilibrium." Sibling facts (nonnegativity, evaluation identities, canonical threshold positivity) and the inhabited falsifiability certificate build on that scalar. In the forcing chain it sits under T5: once $J$ is unique, every domain comparison is forced to use the same cost. Downstream used-by edges are empty in the graph snapshot, so its immediate consumers are the in-module certificate constructors rather than external theorems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.