domainCost
plain-language theorem explainer
Domain cost assigns to a pair of reals (m,e) the recognition cost of their ratio m/e. The magnetar structural module uses it as the local cost on mass-energy quotients. It 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 $J(m/e)$, where $J(x)=\frac{x+x^{-1}}{2}-1$ is the recognition cost of a positive ratio.
background
Module 11 is the structural magnetar-field layer of RS astrophysics (target scale $\phi^{72}$ Gauss $\sim 10^{14}$ Gauss, zero sorry, zero axiom). The ambient cost is the J-functional forced by the Recognition Composition Law and uniqueness (T5): $J(x)=\frac12(x+x^{-1})-1$. Upstream modules (Cost, Cosmology.RefineTrigger, Gravity bridges, SpiralField) all expose the same Jcost as "the RS recognition cost of a positive ratio," with the EnergyProcessingBridge doc stressing uniqueness under RCL.
Domain cost simply feeds the dimensionless quotient $m/e$ into that functional. In this module the pair $(m,e)$ is the natural mass-energy argument before thresholds and certificates are stated.
proof idea
Definitional one-liner: the body is exactly $J(m/e)$. No tactics, no lemmas, no side conditions in the definition itself.
why it matters
Gives the module its local cost symbol so sibling facts (evaluation at equality, nonnegativity, canonical threshold positivity) and the structural certificate RSAstro011Cert can speak uniformly. Anchors the magnetar structural claim to the global J-uniqueness landmark (T5) and the RCL rather than an ad-hoc astrophysical cost. No external used-by edges yet; value is internal to the Module 11 certificate chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.