domainCost
plain-language theorem explainer
Domain cost of a mass scale m against an energy scale e is the recognition cost of their ratio: J(m/e). Gravity and structural proofs cite it whenever a dimensionless mass-to-energy mismatch must be scored by the unique RS cost. The body is a one-line definitional wrapper around Jcost.
Claim. For real $m$ and $e$, the domain cost is $J(m/e)$, where the recognition cost is $J(x)=\frac{x+x^{-1}}{2}-1$.
background
This module records structural facts about the RS J-cost in a gravity setting, with emphasis on ratio symmetry $J(x)=J(1/x)$. Status is fully closed: zero sorry, zero axioms.
The cost functional is the unique nonnegative functional forced by the Recognition Composition Law: $J(x)=\frac{1}{2}(x+x^{-1})-1$ for $x>0$ (equivalently $\cosh(\log x)-1$). Upstream definitions across Cost, CoherenceCollapse, and EnergyProcessingBridge all pin the same formula and note that a genuine distinction (ratio not one) has strictly positive cost.
Here the two arguments are a mass-like scale $m$ and an energy-like scale $e$. Their ratio is the natural dimensionless input to $J$, so domain cost is simply that evaluation.
proof idea
Pure definition: domainCost m e is definitionally Jcost (m / e). No lemmas, tactics, or side conditions appear in the body. Nonnegativity, evaluation identities, and threshold comparisons live in sibling declarations.
why it matters
Structural Module 7 packages the ratio-symmetric recognition cost for gravity use. Domain cost is the local name for scoring a mass-to-energy mismatch by the T5-unique J functional, so later structural certificates (canonical thresholds, nonnegativity, the RSGRVStructural007 cert) can speak in gravity variables without reopening the cost definition.
It sits on the forcing chain landmark T5 (J-uniqueness from the Recognition Composition Law) and feeds the module's claim that recognition cost is ratio-symmetric. No downstream edges are recorded yet; the immediate consumers are the sibling lemmas in the same file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.