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 structural forcing chain or threshold lemmas in this module cites it as the local cost functional. It is a one-line abbreviation of the unique J-cost forced by the Recognition Composition Law.
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 fixes a unique cost on positive ratios via the Recognition Composition Law. That cost is $J(x) = \frac{x + x^{-1}}{2} - 1$, equivalently $\cosh(\log x) - 1$. Upstream modules (Cost, CoherenceCollapse, EnergyProcessingBridge, RefineTrigger, SpiralField) all expose the same $J$ under the name Jcost; EnergyProcessingBridge records that it is the unique functional forced by RCL.
This module sits in the structural forcing chain after T5 (J-uniqueness) and T6 ($\varphi$ forced as the self-similar fixed point), heading toward T7 (eight-tick octave) and T8 ($D = 3$). Domain cost simply specializes $J$ to a mass-over-energy ratio, the natural dimensionless argument when comparing a mass scale to an energy scale in the same units.
Sibling lemmas in the file (non-negativity, evaluation identities, a canonical threshold) treat this specialization as the working cost on the domain.
proof idea
Pure definitional abbreviation: domainCost m e is defined to be Jcost (m / e). No proof obligations; the body is the single application of the shared J-cost functional to the ratio m/e.
why it matters
Gives the module a named cost on mass-energy pairs so later structural statements (non-negativity, threshold positivity, the RSFDNStructural009 certificate) can speak in domain language rather than raw J. It sits downstream of T5 J-uniqueness in the forcing chain and inherits the RCL-forced form $J(x) = (x + x^{-1})/2 - 1$. No downstream consumers are wired yet in the graph; the immediate consumers are the sibling lemmas and the module certificate that package the structural claims for this foundation slice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.