domainCost
plain-language theorem explainer
Domain cost assigns the recognition cost of a mass-to-energy ratio by evaluating the J-functional at m/e. Anyone working the RS fine-structure or scale-comparison layer cites it as the local cost of a dimensional mismatch. The body is a one-line specialization of the standard J-cost.
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
Recognition Science measures mismatch of positive scales by the J-cost $J(x)=\frac{x+x^{-1}}{2}-1$, also written $\cosh(\log x)-1$. Upstream modules (Cost, Cosmology.RefineTrigger, Gravity.CoherenceCollapse) all fix this same functional: it vanishes only at ratio one and is nonnegative for $x>0$.
This module is Physics RS Module 2, the structural EM fine-structure certificate: $\alpha^{-1}$ forced into $(137.030,137.039)$ with CODATA $137.036$ inside, status RS_PASS and zero sorry. Domain cost is the local bridge that turns a raw mass/energy pair into a J-value before thresholds or certificates are applied.
Sibling material in the same file (nonnegativity of domain cost, a canonical positive threshold, and the RSPhysics002Cert package) builds directly on this definition.
proof idea
Pure definition: one-line abbreviation that feeds the ratio $m/e$ into the already-defined J-cost. No tactics, no lemmas, no proof obligations.
why it matters
Gives the Physics module a named cost for comparing a mass scale to an energy scale under the same J that appears in the forcing chain (T5 J-uniqueness) and the Recognition Composition Law. Downstream siblings use it for nonnegativity, a positive canonical threshold, and the inhabited RSPhysics002Cert that packages the alpha-band structural theorem. Without a shared domain cost, the fine-structure certificate would have to re-inline $J(m/e)$ at every call site. It does not itself prove the alpha interval; it only supplies the cost primitive that certificate and threshold lemmas sit on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.