domainCost
plain-language theorem explainer
The domain cost of a mass-energy pair is the recognition cost of their ratio: J(m/e). Anyone working the D=3 configuration-space metric or threshold comparisons cites this. It is a one-line abbreviation of the unique J-cost on the positive ratio 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
The module fixes configuration space at spatial dimension $D=3$: $C_3 = \mathbb{R}^3$ equipped with the recognition metric $ds^2 = J(dx/x)$ on the positive orthant. That metric is positive definite for all $x > 0$.
The cost functional is the unique $J$ forced by the Recognition Composition Law (forcing chain T5): $J(x) = \frac{x + x^{-1}}{2} - 1$, also written $\cosh(\log x) - 1$. Upstream copies of $J$ state that a genuine distinction (ratio not one) has strictly positive cost, and that $J$ is nonnegative on positives.
Domain cost specializes $J$ to a mass-to-energy ratio $m/e$, the natural dimensionless argument when comparing scales inside the configuration-space geometry.
proof idea
Pure definitional abbreviation: apply $J$ to the quotient $m/e$. No lemmas, no tactics.
why it matters
Gives the scalar cost that the D=3 configuration-space development compares against thresholds. Sibling facts (nonnegativity of domain cost, evaluation identities, the canonical threshold and its positivity, and the ConfigSpaceD3 certificate) all sit on this abbreviation. It ties the local Riemannian picture to the global J-uniqueness step (T5) and to the forced $D=3$ landmark (T8) of the forcing chain. No downstream theorem edges are recorded yet; the immediate consumers are the in-module certificate and threshold lemmas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.