domainCost
plain-language theorem explainer
Defines the astrophysical domain cost of a mass-to-energy ratio as the RS J-cost of m/e. Anyone comparing solar or stellar scales against Recognition thresholds cites this wrapper. It is a one-line abbreviation of the unique cost functional forced by the Recognition Composition Law.
Claim. For real $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 measures mismatch of positive ratios by the J-cost $J(x)=\frac12(x+x^{-1})-1$, equivalently $\cosh(\log x)-1$. Upstream modules record that this is the unique cost forced by the Recognition Composition Law (RCL), and that $J(x)\ge 0$ for $x>0$ with equality only at $x=1$.
This module is Astrophysics RS Module 1, whose structural claim is that the solar surface temperature equals $\phi^{18},\mathrm{K}=5778,\mathrm{K}$ (PDG exact). Domain cost supplies the local cost of a mass-to-energy ratio against which canonical thresholds in the same file are compared.
Notation: $m$ and $e$ are bare reals; positivity and nondegeneracy of $e$ are left to callers (siblings such as nonnegativity lemmas).
proof idea
Pure definitional abbreviation: expand domainCost m e to Jcost (m / e). No tactics, no lemmas. The body is the standard J-cost applied to the ratio $m/e$.
why it matters
Gives the astrophysics layer a uniform cost on mass-energy ratios so later certificates (canonical thresholds, the RSAstro001Cert package) can state nonnegativity and exact solar matches without re-deriving J. Ties the module to the forcing chain landmark T5 (J-uniqueness) and to RCL. No downstream users are wired yet in the graph; siblings domainCost_nonneg and canonicalThreshold are the immediate consumers inside the same file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.