domainCost
plain-language theorem explainer
Domain cost assigns the recognition cost of a mass-to-energy ratio: J(m/e) with the standard J-cost. Anyone bounding ladder costs or thresholds in the J-cost bounds module cites it as the local cost functional. The body is a one-line abbreviation of Jcost on the quotient.
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 module develops structural J-cost bounds on the phi-ladder: $J(\varphi^k)=(\varphi^k+\varphi^{-k})/2-1=L_k/2-1$ in terms of Lucas numbers, with explicit values $J(1)=0$, $J(\varphi)$, $J(\varphi^2)\approx 0.809$, $J(\varphi^3)\approx 1.238$. Status is a structural theorem package (no sorry, no axioms).
Upstream, the recognition cost is the unique T5 functional $J(x)=\frac{1}{2}(x+x^{-1})-1$ (also written $\cosh(\log x)-1$). Doc-comments state it as the RS cost of a positive ratio, strictly positive off the identity, and nonnegative for $x>0$. Domain cost simply specializes that functional to a mass-over-energy ratio, the natural dimensionless argument when comparing a mass scale to an energy (or yardstick) scale on the ladder.
proof idea
Pure definition: one-line abbreviation that applies the imported J-cost to the quotient $m/e$. No proof obligations.
why it matters
Gives the local cost functional for the J-cost bounds v3 session. Sibling lemmas (nonnegativity, evaluation identities, canonical threshold positivity, and the module certificate) are stated in terms of this abbreviation, so the rest of the file can talk about mass/energy ratios without repeating $J(m/e)$. In the broader framework it is the T5 J-cost evaluated on a dimensionless ratio, the same object that appears in the Recognition Composition Law and in ladder mass formulas. No downstream dependents are wired yet; the declaration is infrastructure inside Foundation.JCostBounds3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.