domainCost
plain-language theorem explainer
Defines the domain cost of a mass-to-energy ratio as the recognition cost J(m/e). Astrophysicists working the stellar-metallicity match in RS Module 7 cite it as the local cost functional on mass-energy pairs. The body is a one-line abbreviation of the standard J-cost on the quotient.
Claim. For real numbers $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) = \frac{x + x^{-1}}{2} - 1$, equivalently $\cosh(\log x) - 1$. Upstream modules (Cost, CoherenceCollapse, EnergyProcessingBridge, RefineTrigger, SpiralField) all expose the same functional; EnergyProcessingBridge records that it is the unique cost forced by the Recognition Composition Law.
This module (Astrophysics RS Module 7) targets stellar metallicity: the structural claim is $J(\varphi)^2 \approx 0.0139$, matching solar metallicity $Z_\odot \approx 0.014$. Domain cost specializes J to a mass-energy pair $(m,e)$, so metallicity and related abundance ratios can be scored in the same units as the rest of the forcing chain.
proof idea
Pure definitional abbreviation: domainCost m e is definitionally Jcost (m / e). No tactics, no lemmas, no proof obligations.
why it matters
Gives Module 7 a named cost on mass-energy ratios so later certificates (domainCost_nonneg, canonicalThreshold, RSAstro007Cert) can talk about nonnegativity and thresholds without reopening the J formula. Ties the stellar-metallicity MATCH line to the T5 J-uniqueness landmark and the RCL-forced cost. No downstream users are wired yet in the graph; the immediate consumers are the sibling lemmas in the same module that discharge nonnegativity and the inhabited certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.