domainCost
plain-language theorem explainer
Domain cost of a mass-scale pair (m, e) is the recognition cost of their ratio m/e. Module-11 rung-spacing arguments cite it as the local cost on consecutive phi-rungs. It is a one-line abbreviation of the forced J-functional applied to m/e.
Claim. For real $m$ and $e$, the domain cost is $J(m/e)$, where $J(x)=\frac{x+x^{-1}}{2}-1$.
background
Foundation Module 11 treats RS rung spacing: consecutive rungs on the phi-ladder differ by the fixed factor $\phi\approx 1.618$. Status is structural (zero sorry, zero axiom).
The recognition cost $J$ is the unique functional forced at T5 of the forcing chain: $J(x)=\frac{x+x^{-1}}{2}-1$ (equivalently $\cosh(\log x)-1$). Upstream docs state it is the RS cost of a positive ratio, vanishes only at ratio one, and is nonnegative for positive $x$.
Here a mass-like quantity $m$ is compared to an energy-like scale $e$. Their dimensionless ratio $m/e$ is the natural argument of $J$.
proof idea
Definitional abbreviation only: domain cost is exactly $J$ evaluated at the quotient $m/e$. No lemmas, no tactics, no proof obligations.
why it matters
Local cost measure for the structural theorems of Module 11 on phi-rung spacing. Sibling results (nonnegativity, equality at matched scales, canonical threshold) build directly on this abbreviation. Anchors the T5 J-uniqueness landmark inside the rung-spacing setting and feeds the module certificate. No external used-by edges yet; it is in-module infrastructure for the forcing-chain rung step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.