domainCost
plain-language theorem explainer
Defines the domain cost of a mass-scale pair as the Recognition J-cost of their ratio: J(m/e). Anyone working the structural cost layer or the golden-ratio minimum cites this 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 cost of a positive ratio.
background
Recognition Science measures the cost of a positive scale ratio by the functional $J(x)=\frac{x+x^{-1}}{2}-1$, equivalently $\cosh(\log x)-1$. Upstream modules (Cost, Cosmology.RefineTrigger, Gravity.CoherenceCollapse) all expose this same $J$ as Jcost, with the standing facts that $J(1)=0$ and $J(x)>0$ for $x\neq 1$ when $x>0$.
This module is Foundation RS Structural Module 2. Its stated setting is the J-cost minimum at the golden ratio: $J(\varphi)=\varphi-3/2\approx 0.11803$, the golden-ratio recognition cost, with structural status (zero sorry, zero axiom).
Domain cost simply specializes $J$ to a pair of real parameters $(m,e)$ by feeding the ratio $m/e$. That is the natural cost of treating $m$ relative to a reference scale $e$ inside the structural layer.
proof idea
Pure definition: one-line abbreviation. No tactics, no lemmas. The body is exactly $J(m/e)$ via the shared Jcost functional from Cost (and the identical copies in Cosmology and Gravity).
why it matters
Gives the module a named cost on mass/energy-style pairs so sibling lemmas (domainCost_nonneg, domainCost_at_eq, canonicalThreshold) can talk about non-negativity and the golden-ratio threshold without reopening the formula for $J$.
In the forcing chain this sits under T5 J-uniqueness: $J(x)=\frac{x+x^{-1}}{2}-1$ is the unique cost compatible with the Recognition Composition Law. The module headline minimum $J(\varphi)=\varphi-3/2$ is the self-similar fixed-point cost tied to T6 ($\varphi$ forced). No downstream used_by edges are recorded yet; the definition is local scaffolding for the structural certificate RSFDNStructural002Cert and the canonical threshold facts in the same file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.