domainCost
plain-language theorem explainer
Domain cost assigns to a mass–energy pair the recognition cost of their ratio: J(m/e). Gravity and structural-RS authors cite it when a dimensionless mass-to-energy mismatch must be scored by the unique J-cost. The body is a one-line abbreviation of Jcost applied to m/e.
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 scores dimensionless mismatches with the J-cost $J(x)=\frac{1}{2}(x+x^{-1})-1$. Upstream modules (Cost, EnergyProcessingBridge, CoherenceCollapse) fix this functional as the unique cost forced by the Recognition Composition Law; it vanishes only at ratio one and is nonnegative for $x>0$.
This file is Gravity RS Structural Module 5. The module framing is the eight-tick octave: one full traversal of the binary recognition lattice with period $2^D=8$ (T7). Domain cost is the local shorthand that feeds mass and energy into that cost before thresholds and certificates are stated.
proof idea
Pure definitional abbreviation: domainCost m e is defined to be Jcost (m / e). No tactics, no lemmas, no proof obligations.
why it matters
Gives the structural gravity stack a named mass–energy cost before nonnegativity (domainCost_nonneg), evaluation identities (domainCost_at_eq), and the canonical threshold / RSGRVStructural005Cert siblings. Ties gravity bookkeeping to the T5 J-uniqueness landmark and the eight-tick setting of the module. No downstream used_by edges are recorded yet; the def is infrastructure for those local certificates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.