domainCost
plain-language theorem explainer
Defines the domain cost of a mass-to-energy style ratio as the recognition cost J of that ratio. Anyone comparing RS cost structure to traffic or capacity ratios cites this. The body is a one-line abbreviation of Jcost applied to m/e.
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 frames annual internet traffic growth against the golden ratio: historical Cisco growth near $1.58\times$/yr versus the RS self-similar fixed point $\varphi \approx 1.618$ (about $2.4%$ off). Status is structural: no sorry, no axioms.
The recognition cost $J$ is the unique nonnegative functional forced by the Recognition Composition Law, $J(x) = \frac{x + x^{-1}}{2} - 1$ (equivalently $\cosh(\log x) - 1$). Upstream definitions across Cost, Cosmology, Gravity, and Spiral all pin the same formula: cost of a genuine distinction (ratio not one) is strictly positive for $x > 0$.
Domain cost simply specializes that functional to a two-argument ratio $m/e$, the natural input when comparing measured growth or capacity scales inside the information layer.
proof idea
Pure definitional abbreviation: expand to $J(m/e)$ with the standard $J$-cost. No tactics, no lemmas, no proof obligations.
why it matters
Gives the information module a named handle on RS cost for traffic-style ratios, so later certificates (canonical threshold positivity, InternetTrafficCert) can speak in cost language rather than raw ratios. Ties the internet-growth comparison to the same $J$ forced at T5 in the unified forcing chain and used throughout Cost and Gravity. No downstream dependents are wired yet; this is the local cost primitive for the structural traffic certificate stack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.