domainCost
plain-language theorem explainer
Domain cost of a mass m against an energy scale e is the recognition cost of the ratio m/e. GUT-scale and ladder arguments in RS cite it whenever a mass is scored relative to a reference energy. The body is a one-line abbreviation of the unique J-cost on that ratio.
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 ambient module fixes the RS reading of the grand-unification scale: $M_{\mathrm{GUT}}\sim 2\times 10^{16},\mathrm{GeV}$ is written as $M_Z\cdot\varphi^{r}$ with rung $r\approx 74.5$, so $M_{\mathrm{GUT}}=M_Z\cdot\varphi^{74.5}$. The development is marked structural (no sorry, no axioms).
The cost functional used here is the standard RS J-cost $J(x)=\frac{1}{2}(x+x^{-1})-1$. Upstream docs identify it as the unique cost forced by the Recognition Composition Law, non-negative for $x>0$, and strictly positive when the ratio is not one. Domain cost simply evaluates that functional on the dimensionless ratio of a mass to an energy scale.
proof idea
Pure definition: apply J-cost to the ratio $m/e$. No lemmas, no tactics; the body is the abbreviation $J(m/e)$.
why it matters
Gives the local cost primitive for the GUT-scale RS v3 session. Sibling facts (non-negativity, evaluation identities, the canonical threshold, and the module certificate) sit on top of this abbreviation, so any structural claim that a mass sits above or below a GUT-domain threshold is scored through this map.
Framework landmark: T5 J-uniqueness forces $J(x)=\cosh(\log x)-1$, equivalently $\frac{x+x^{-1}}{2}-1$, so domain cost inherits the RCL-forced cost rather than an ad-hoc penalty. The phi-ladder mass formula and the GUT rung $\approx 74.5$ are the intended consumers; used_by is empty in the graph snapshot, but the sibling certificate bundle is the immediate landing site.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.