domainCost
plain-language theorem explainer
Domain cost assigns to a mass–energy pair the recognition cost of their ratio m/e. Structural gravity arguments in the RS count-law module use it as the penalty for a mass scale relative to an energy scale. The definition is a one-line application of the unique J-cost functional forced by the Recognition Composition Law.
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
Recognition Science measures mismatch of positive scales by the J-cost $J(x)=\frac{x+x^{-1}}{2}-1$. Upstream modules record that this is the unique cost forced by the Recognition Composition Law (T5), and that $J(x)\ge 0$ for $x>0$ with equality only at $x=1$.
This module is Gravity RS Structural Module 3. Its setting is the RS count law: from spatial dimension $D=3$ one obtains $2^D-1=7$ independent channels, treated as a structural theorem with no sorry and no axioms.
Domain cost specialises $J$ to a mass-over-energy ratio. Sibling lemmas then record evaluation at equality and non-negativity, and feed a canonical threshold used by the module certificate.
proof idea
Pure definition: substitute the ratio $m/e$ into the standard J-cost. No tactics, no lemmas beyond the imported $J$ abbreviation itself.
why it matters
Gives the gravity stack a named cost for comparing a mass scale to an energy scale inside the structural count-law module ($2^D-1=7$ channels from $D=3$). It sits under T5 J-uniqueness and the RCL-forced form $J(x)=\cosh(\log x)-1$. Siblings domainCost_nonneg and canonicalThreshold build on it toward the module certificate RSGRVStructural003Cert. No external used-by edges are recorded yet; the definition is local scaffolding for those structural claims rather than a global mass formula or GR matching theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.