domainCost
plain-language theorem explainer
The domain cost of a mass–energy pair is the recognition cost of their ratio: J(m/e). CPT and threshold arguments in this module cite it as the scalar that measures how far a kinematic ratio sits from unity. The definition is a one-line specialization of the unique J-cost forced by the Recognition Composition Law.
Claim. For real numbers $m$ and $e$, the domain cost is $\mathrm{domainCost}(m,e) := J(m/e)$, where $J(x) = \frac{1}{2}(x + x^{-1}) - 1$ is the recognition cost of a positive ratio.
background
This module develops CPT as a structural theorem in Recognition Science: combined charge conjugation, spatial reflection (D = 3), and tick reversal leave physics invariant precisely because the J-cost is unchanged under those maps. The status line is structural (0 sorry, 0 axiom).
The unique cost functional forced by the Recognition Composition Law is $J(x) = \frac{1}{2}(x + x^{-1}) - 1$ (equivalently $\cosh(\log x) - 1$), the T5 landmark. Upstream modules define the same $J$ as the RS recognition cost of a positive ratio; a genuine distinction (ratio not one) has strictly positive cost, and $J$ is nonnegative for $x > 0$.
Domain cost simply feeds the mass-to-energy ratio into that functional, so later lemmas can talk about kinematic imbalance without repeating the $J$ formula.
proof idea
Pure definitional abbreviation: expand as $J(m/e)$ with the standard $J$-cost. No proof obligations; downstream facts (nonnegativity, evaluation at equality, threshold comparisons) inherit from properties of $J$.
why it matters
Gives the module a named scalar for “how costly is this mass–energy domain ratio,” which is the natural input to CPT invariance phrased as J-cost invariance under C, P, and T. Siblings such as nonnegativity of domain cost, the equality case, the canonical threshold, and the CPT3 certificate package sit on top of this abbreviation.
In the forcing chain, J-uniqueness (T5) and the Recognition Composition Law fix the functional; specializing it to $m/e$ is the bridge from abstract cost to the CPT structural claim in this file. No downstream edges are recorded yet outside the module siblings, so its immediate role is local scaffolding for the CPT certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.