domainCost
plain-language theorem explainer
Defines the domain cost of a mass-energy pair as the recognition cost of their ratio. Astrophysicists working the RS solar-radius ladder (Module 8) cite it as the local cost functional on dimensionless ratios. The body is a one-line abbreviation of Jcost applied to m/e.
Claim. For real numbers $m$ and $e$, the domain cost is $J(m/e)$, where the recognition cost is $J(x)=\frac{x+x^{-1}}{2}-1$.
background
Recognition Science measures mismatch of positive ratios by the J-cost $J(x)=\frac{1}{2}(x+x^{-1})-1$. Upstream definitions (Cost, CoherenceCollapse, EnergyProcessingBridge, RefineTrigger, SpiralField) all fix the same functional; EnergyProcessingBridge notes it is the unique cost forced by the Recognition Composition Law, matching forcing-chain step T5.
This module (RS Astrophysics Module 8) treats the solar radius as a structural match: $\varphi^{43},\mathrm{m}\approx 7.0\times 10^8,\mathrm{m}$ versus $R_\odot=6.96\times 10^8,\mathrm{m}$ (0.6%). Domain cost supplies the local scalar that later lemmas (nonnegativity, equality-at-unity, canonical threshold) use when comparing mass and energy scales on that ladder.
proof idea
Pure definition: no proof obligations. The body is the term Jcost (m / e), i.e. the standard recognition cost evaluated at the dimensionless ratio of the two real arguments.
why it matters
Gives Module 8 a named cost on mass-energy ratios so sibling lemmas (domainCost_nonneg, domainCost_at_eq, canonicalThreshold) can state positivity and threshold facts without reopening the J-cost definition. Anchors the solar-radius structural match to the same T5 J-functional used across cosmology, gravity, and spiral modules. No downstream theorems yet list this def as a dependency; it is infrastructure for the module certificate RSAstro008Cert.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.