domainCost
plain-language theorem explainer
Defines the domain cost of a mass–energy pair as the recognition cost of their ratio: J(m/e). Gravity and structural-threshold arguments cite it when comparing a mass scale to an energy scale under the RS cost functional. The body is a one-line abbreviation of the standard J-cost on the quotient.
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
This module is Gravity RS Structural Module 2. It records structural facts about the RS J-cost, including that the cost attains its golden-ratio minimum $J(\varphi)=\varphi-3/2\approx 0.11803$. Status is structural: zero sorry, zero axioms.
The recognition cost $J$ is the unique functional forced by the Recognition Composition Law (T5): $J(x)=\frac{x+x^{-1}}{2}-1$ for $x>0$. Upstream copies of $J$ (Cost, CoherenceCollapse, EnergyProcessingBridge, etc.) all use that same formula; EnergyProcessingBridge notes it is the unique cost forced by RCL. A genuine distinction (ratio not one) has strictly positive cost.
Domain cost simply specializes $J$ to the mass-to-energy ratio $m/e$, the natural dimensionless argument when a gravitational or structural threshold compares a mass scale to an energy scale.
proof idea
Pure definition: one-line abbreviation. No tactics or lemmas. The body substitutes the ratio $m/e$ into the standard $J$-cost $J(x)=\frac{x+x^{-1}}{2}-1$.
why it matters
Gives the module a named mass–energy cost so later structural lemmas (non-negativity, value at equality, canonical threshold positivity, and the RSGRVStructural002 certificate) can speak in gravity language rather than raw $J$. It sits under the T5 J-uniqueness landmark and the module’s golden-ratio minimum $J(\varphi)=\varphi-3/2$. No downstream uses are wired yet in the graph; the immediate consumers are the sibling facts in this file that build the structural certificate around that minimum.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.