domainCost
plain-language theorem explainer
Domain cost of a mass-to-energy pair is the recognition cost J of their ratio. Cited in the RS white-dwarf module when packaging structural cost bounds. One-line abbreviation of J applied to m/e; no proof content.
Claim. For real $m$ and $e$, the domain cost is $J(m/e)$, where $J(x)=\frac{x+x^{-1}}{2}-1$.
background
Recognition Science measures the cost of a positive ratio $x$ by $J(x)=\frac{x+x^{-1}}{2}-1$ (equivalently $\cosh(\log x)-1$). Upstream, this is the unique cost forced by the Recognition Composition Law and recorded as T5 in the forcing chain; the same Jcost appears in Cost, Cosmology.RefineTrigger, and Gravity.CoherenceCollapse.
This module (Astrophysics RS Module 5) is a structural theorem for white-dwarf radius: $\phi^{19}\cdot 0.75,\mathrm{km}=7012,\mathrm{km}\approx 7000,\mathrm{km}$, with zero sorry and zero axioms. Domain cost is the local packaging of $J$ on a mass-to-energy ratio for that setting.
proof idea
Definitional abbreviation only: domainCost m e is exactly Jcost (m / e). No tactics, no lemmas, no proof obligations.
why it matters
Gives the cost primitive used by sibling facts domainCost_nonneg and domainCost_at_eq, and by the module certificate RSAstro005Cert for the white-dwarf radius match. Anchors the astrophysical scale to the universal J-cost of T5 (and thus to RCL). No external used_by edges yet; the def is local infrastructure for the module's structural claims.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.