domainCost
plain-language theorem explainer
Domain cost assigns to a mass–energy pair the recognition cost of their ratio: J(m/e). Nuclear-shell arguments in RS cite it as the scalar that compares a particle mass against a reference energy before thresholds and shell certificates are applied. The body is a one-line abbreviation of the forced J-cost on the positive ratio m/e.
Claim. For real numbers $m$ and $e$, the domain cost is $J(m/e)$, where the recognition cost is $J(x)=\frac{x+x^{-1}}{2}-1$ (for $x\neq 0$).
background
The ambient module builds the nuclear shell model from J-cost: single-particle orbital families (s${1/2}$, p${1/2}$, p${3/2}$, d${3/2}$, d$_{5/2}$) are identified with the five-dimensional configuration space forced at $D=3$, so configDim $D=5$. Status is structural (no sorry, no axioms).
The only primitive used here is the recognition cost $J$. Across Cost, Cosmology, Gravity, and Spiral it is the same functional $J(x)=\frac12(x+x^{-1})-1$, forced by the Recognition Composition Law (T5 uniqueness). Upstream docs state it is the unique cost of a positive ratio and is nonnegative for $x>0$; a genuine distinction (ratio not one) has strictly positive cost.
Domain cost simply specializes that functional to a mass-over-energy ratio, the natural dimensionless input for nuclear level comparisons in RS-native units.
proof idea
Pure definition: no proof obligations. The right-hand side applies the shared noncomputable $J$-cost to the quotient $m/e$. Downstream lemmas in the same file (nonnegativity, evaluation identities, canonical threshold) inherit whatever positivity and algebraic properties $J$ already has on positive reals.
why it matters
This is the scalar interface between particle masses and the J-cost machinery inside the nuclear shell development. Sibling results (domain-cost nonnegativity, equality-at-evaluation, canonical threshold positivity, and the NuclearShell3 certificate) all read domain cost as their cost input; without a named mass/energy cost there is nothing to threshold against shell occupancy.
Framework landmarks: it inherits T5 J-uniqueness and the RCL form of $J$, and sits under the nuclear reading of configDim $D=5$ (five orbital families). It does not itself force magic numbers or close the shell certificate; it only standardizes the cost that those later objects consume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.