domainCost
plain-language theorem explainer
The domain cost of a mass-to-energy ratio is the recognition cost J of that ratio. Anyone working the RS entanglement-cost layer cites it as the elementary cost assigned to a domain scale pair (m, e). The declaration is a one-line definitional wrapper around J.
Claim. For real numbers $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
The module treats entanglement entropy in Recognition Science units. Classical Shannon form $S = -\sum p_k \log p_k$ is retained; the RS bound is $S_{\max} = D \log 2 = 3\log 2 \approx 2.079$ bits, identified with Count Law bits in three spatial dimensions (forcing step T8).
The unique cost functional forced by the Recognition Composition Law is $J(x) = \frac12(x + x^{-1}) - 1$ (equivalently $\cosh(\log x) - 1$). Upstream modules record that a genuine distinction (ratio not one) has strictly positive cost, and that $J$ is nonnegative for positive arguments. Domain cost simply evaluates that functional on a mass-to-energy ratio $m/e$, the natural dimensionless scale for a domain in the RS ledger.
proof idea
Pure definition: domainCost m e is defined to be Jcost (m / e). No proof obligations; the body is the standard J-cost applied to the quotient.
why it matters
Gives the elementary cost assignment used throughout the entanglement-cost certificate layer of the foundation. Sibling facts (nonnegativity, evaluation identities, the canonical threshold) build directly on this abbreviation. In the broader forcing chain it sits under T5 J-uniqueness and the Recognition Composition Law: once $J$ is forced, every domain scale pair inherits a unique nonnegative cost. The module status is structural (zero sorry, zero axiom), so this definition is part of the closed skeleton rather than scaffolding. Downstream certificates compare domain cost against entanglement thresholds tied to $S_{\max} = 3\log 2$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.