domainCost
plain-language theorem explainer
Domain cost assigns the recognition cost J to a mass-to-energy (or abundance) ratio m/e. The carbon-oxygen stellar module uses it when scoring C/O against the phi-ladder target φ^{-1.5}. It is a one-line definitional wrapper of the unique J-cost functional.
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
Astrophysics RS Module 12 is a structural (zero-sorry) treatment of carbon-oxygen stellar chemistry. The module narrative fixes the target abundance C/O = φ^{-1.5} ≈ 0.504 against the observed ~0.55 (about 10% off) and packages the comparison as a certificate.
The recognition cost J is the unique functional forced by the Recognition Composition Law: J(x) = (x + x^{-1})/2 - 1. Upstream copies state that a genuine distinction (ratio not one) has strictly positive cost and that J is nonnegative for positive arguments. Domain cost simply feeds the ratio m/e into that functional, so stellar abundance mismatches become J-costs on the same footing as other RS domains.
proof idea
Definitional abbreviation only: domainCost m e is defined as Jcost (m / e). No tactics, no lemmas, no proof body.
why it matters
Gives the module a named cost on abundance (or mass-energy) ratios so sibling lemmas can prove nonnegativity, evaluate at equality, and compare against a canonical threshold en route to RSAstro012Cert. That certificate is the structural claim that C/O sits on the phi-ladder at rung offset -1.5. The construction sits on T5 J-uniqueness (J(x) = cosh(log x) - 1) and the broader phi-ladder mass formula; without a domain-level J, the stellar ratio would not speak the same cost language as cosmology and gravity bridges in the monolith.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.