domainCost
plain-language theorem explainer
The domain cost of a mass-energy pair is the recognition cost of their ratio: J(m/e). Anyone working the RS 2026 state certificate or threshold lemmas cites this as the local cost on a mass-to-energy scale. The body is a one-line abbreviation of the unique J-cost functional on the positive ratio m/e.
Claim. For real numbers $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
Recognition Science forces a unique nonnegative cost on positive ratios. That functional is $J(x) = \frac{x + x^{-1}}{2} - 1$, equivalently $\cosh(\log x) - 1$, fixed by the Recognition Composition Law and the T5 uniqueness step of the forcing chain. Upstream modules (Cost, CoherenceCollapse, EnergyProcessingBridge, RefineTrigger, SpiralField) all expose the same $J$ under the name Jcost; EnergyProcessingBridge records that it is "the unique cost functional forced by the Recognition Composition Law."
This module packages the 2026 structural state of the art: forcing chain T0–T8 complete, constants derived, zero sorry. Domain cost specializes $J$ to a mass-over-energy ratio, the natural dimensionless argument when comparing a mass scale $m$ to an energy scale $e$ inside threshold and certificate lemmas that sit beside this definition.
proof idea
Pure definitional abbreviation: domainCost is defined to be Jcost applied to the ratio m/e. No tactics, no lemmas, no proof obligations. Downstream nonnegativity and evaluation lemmas (siblings domainCost_nonneg, domainCost_at_eq) inherit directly from the corresponding properties of J.
why it matters
Gives the RS 2026 certificate module a named mass-energy cost rather than raw Jcost calls. Siblings use it for nonnegativity (domainCost_nonneg), evaluation identities (domainCost_at_eq), and the canonical threshold apparatus (canonicalThreshold, canonicalThreshold_pos) that feed the inhabited certificate RS2026State3Cert. Framework-wise it is the local face of T5 J-uniqueness: every genuine distinction of scale carries positive cost, and the mass-to-energy ratio is the scale that thresholds and coherence arguments need. No used_by edges are recorded yet; the definition is scaffolding for the certificate block rather than a leaf of a larger proof tree.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.