domainCost
plain-language theorem explainer
Domain cost assigns the recognition cost of a mass-to-energy ratio: J(m/e) with the forced J-cost. Anyone working the RS structural rung-spacing module cites it as the local cost on a mass/energy pair. The body is a one-line abbreviation of Jcost on the quotient.
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
Module RS_MTH_Structural_008 treats RS rung spacing: adjacent rungs differ by the golden ratio $\varphi\approx 1.618$, and is marked a structural theorem block (no sorry, no axioms).
The underlying cost is the J-functional $J(x)=\frac{1}{2}(x+x^{-1})-1$, the unique cost forced by the Recognition Composition Law (T5). Upstream docs phrase it as "the RS recognition cost of a positive ratio" and note that a genuine distinction (ratio not one) has strictly positive cost; non-negativity for $x>0$ is standard.
Here the ratio is mass over an energy scale, so domain cost is just that J-cost evaluated at $m/e$. Sibling lemmas in the module (evaluation identity, non-negativity, a canonical threshold) build on this abbreviation.
proof idea
Pure definition: unfold to $J(m/e)$ with the standard $J$. No proof obligations; downstream facts (e.g. non-negativity when the ratio is positive) are separate lemmas.
why it matters
Gives the module a named cost on mass/energy pairs so rung-spacing arguments can speak in J-units rather than raw ratios. It sits under the T5 J-uniqueness landmark and the RCL-forced cost $J(x)=\cosh(\log x)-1$. No downstream uses are wired in the graph yet; siblings such as domainCost_nonneg and canonicalThreshold are the immediate consumers inside the structural certificate RSMTHStructural008Cert. The definition itself closes no open question; it is the local vocabulary for the rung-spacing structural claims.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.