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 AllPhysics5 mass or threshold lemmas cites this as the shared scalar cost on a domain. It is a one-line abbreviation of the unique J-cost on the positive ratio m/e.
Claim. For real numbers $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 forces a unique nonnegative cost on positive ratios via the Recognition Composition Law. That cost is $J(x) = \frac12(x + x^{-1}) - 1$, also written $\cosh(\log x) - 1$, and is the T5 landmark in the forcing chain. Upstream modules (Cost, CoherenceCollapse, EnergyProcessingBridge, SpiralField, RefineTrigger) all expose the same $J$ under the name Jcost.
This module, AllPhysics5, is the structural endgame: gravity, EM, weak, strong, Higgs, matter masses, and cosmology are to be read off $J$ with zero free parameters. Domain cost packages the elementary comparison of a mass scale $m$ against an energy scale $e$ as a single $J$-value on the ratio $m/e$, so later threshold and nonnegativity lemmas can stay uniform across sectors.
proof idea
Pure definitional abbreviation: domainCost is defined to be Jcost applied to the quotient $m/e$. No tactics, no lemmas, no proof body.
why it matters
AllPhysics5 claims every physical sector descends from $J$. Domain cost is the local scalar that turns a mass–energy pair into that $J$-value, so sibling facts (equality at a point, nonnegativity, canonical thresholds, and the AllPhysics5 certificate) can speak one language. It sits under T5 J-uniqueness and the RCL identity $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$. No downstream edges are recorded yet; the immediate consumers are the in-module lemmas domainCost_at_eq, domainCost_nonneg, and the threshold/certificate stack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.