domainCost
plain-language theorem explainer
Domain cost of a mass–energy pair is the recognition J-cost of their ratio m/e. Structural work on ratio-symmetric cost (module 7) cites this as the local cost on (m,e). It is a one-line definitional wrapper of the standard J functional.
Claim. For real numbers $m$ and $e$, define the domain cost by $J(m/e)$, where $J(x)=\frac{x+x^{-1}}{2}-1$ is the recognition cost of a positive ratio.
background
Foundation structural module 7 packages the ratio symmetry of recognition cost: $J(x)=J(1/x)$. The ambient claim is that recognition cost depends only on the ratio, not on an absolute scale.
The upstream cost is the standard RS functional $J(x)=\frac{x+x^{-1}}{2}-1$ (equivalently $\cosh(\log x)-1$). Upstream docs call it the unique cost forced by the Recognition Composition Law, and note that a genuine distinction (ratio not one) has strictly positive cost. Domain cost simply specializes that functional to the mass–energy ratio $m/e$.
proof idea
Definitional one-liner: no tactics and no lemmas. The body is exactly $J(m/e)$ with the imported $J$-cost.
why it matters
Gives the local cost object for the structural 007 certificate and its siblings (equality at matched scale, nonnegativity, canonical threshold positivity). In the forcing chain this sits under T5 J-uniqueness and the RCL identity $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$; ratio symmetry $J(x)=J(1/x)$ is the module’s structural theorem. No downstream edges are recorded yet; the def is infrastructure for those sibling lemmas and the inhabited cert.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.