domainCost
plain-language theorem explainer
Domain cost assigns to a mass–energy pair the recognition cost of their ratio. Anyone comparing transistor-scale budgets to the RS cost yardstick in the Moore-law module cites it. The body is a one-line specialization of the unique J-cost to m/e.
Claim. For real $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
The module frames Moore's law in Recognition Science units: transistor count is predicted to grow as $\phi^{2t}$ (annual factor $\phi^2\approx 2.618$), versus the empirical $\sim 2\times$ every 1.5–2 years. Status is structural (no sorry, no axioms).
The underlying cost is the J-functional $J(x)=\frac12(x+x^{-1})-1$, forced uniquely by the Recognition Composition Law (forcing chain T5). Upstream docs state it is the RS recognition cost of a positive ratio, nonnegative for $x>0$, and strictly positive when the ratio is not one.
Domain cost simply evaluates that functional on the mass-to-energy ratio $m/e$, giving a scalar cost for a computational or physical domain characterized by those two scales.
proof idea
Definitional abbreviation only: expand to $J(m/e)$ with the standard J-cost. No lemmas, tactics, or proof obligations.
why it matters
Gives the Moore-law module a named cost on mass–energy pairs so later certificates (nonnegativity, equality at equality of arguments, canonical thresholds, MooreLawCert) can speak in RS units rather than raw ratios. It sits on the T5 J-uniqueness landmark: the same $J$ that appears in cosmology, gravity bridges, and spiral fields is reused here for information scaling. No downstream theorems are wired yet in the graph; the immediate consumers are the sibling lemmas in this file that prove basic properties and build the Moore-law certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.