domainCost
plain-language theorem explainer
Defines the domain cost of a mass-to-energy ratio as the RS recognition cost J of that ratio. Anyone working the structural mass/energy ladder or threshold comparisons in this module cites it as the local cost functional. The body is a one-line abbreviation of Jcost applied to m/e.
Claim. For real $m$ and $e$, the domain cost is $J(m/e)$, where $J(x)=\frac{1}{2}(x+x^{-1})-1$ is the Recognition Science cost of a positive ratio.
background
Recognition Science forces a unique nonnegative cost on positive ratios via the Recognition Composition Law. That cost is $J(x)=\frac12(x+x^{-1})-1$, also written $\cosh(\log x)-1$, and is the T5 uniqueness landmark in the forcing chain. Several modules re-export the same $J$ (Cost, CoherenceCollapse, EnergyProcessingBridge, SpiralField, RefineTrigger); all agree on the formula.
This file is Mathematics RS Structural Module 6, whose stated theme is phi uniqueness as the self-similar fixed point $\varphi=1+1/(1+1/\cdots)$, with structural status (no sorry, no axiom). Domain cost specializes $J$ to a mass-over-energy argument, the natural dimensionless ratio when comparing a mass scale to an energy scale on the phi ladder.
proof idea
Pure definitional abbreviation: domainCost m e is definitionally equal to Jcost (m / e). No lemmas or tactics; the meaning is inherited entirely from the upstream Jcost definition $J(x)=\frac12(x+x^{-1})-1$.
why it matters
Gives the module a named cost on mass/energy ratios so later structural facts (nonnegativity, evaluation identities, canonical thresholds, and the RSMTHStructural006 certificate among the siblings) can speak in domain language rather than raw J. It sits under the T5 J-uniqueness landmark and the RCL-forced cost, and supports the module's phi-uniqueness structural story by measuring how far a ratio sits from the identity cost zero. No downstream consumers are wired yet in the graph; the immediate consumers are the sibling lemmas in this file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.