domainCost
plain-language theorem explainer
Domain cost assigns to a pair of reals (m, e) the recognition cost of their ratio m/e. It is the standard J-cost evaluated at that ratio, so it vanishes exactly when m = e (for positive values) and is nonnegative on the positive ray. Anyone working the D=3 forcing chain or threshold lemmas in Module 6 cites it as the local cost functional. The body is a one-line abbreviation of Jcost.
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 measures mismatch by the J-cost $J(x) = \frac{x + x^{-1}}{2} - 1$ on positive reals. Upstream definitions (Cost, RefineTrigger, CoherenceCollapse) all fix this same functional: it is zero only at ratio one and strictly positive for any genuine distinction.
This module is Foundation RS Module 6. Its stated job is the structural forcing of spatial dimension $D = 3$ from the eight-tick period $2^3$, with no free parameters and zero sorry/axiom debt.
Domain cost simply specializes J to a two-argument interface $(m, e) \mapsto J(m/e)$. Sibling lemmas then record evaluation identities, nonnegativity, and a canonical positive threshold built from that cost.
proof idea
Pure definitional abbreviation: domainCost m e is defined to be Jcost (m / e). No tactics, no lemmas, no proof obligations. Downstream facts (nonnegativity, equality cases) inherit directly from the corresponding properties of Jcost once the ratio is formed.
why it matters
Module 6 sits on the forcing chain that yields $D = 3$ from the eight-tick octave (primer T7–T8). Domain cost is the local cost primitive those structural theorems and the module certificate (RSForcingChain006Cert) can call when they need a mismatch measure between two real scales.
It does not itself force dimension; it only packages J so that threshold and nonnegativity siblings stay readable. With used_by empty in the graph, its immediate consumers are the in-module lemmas domainCost_nonneg, domainCost_at_eq, and canonicalThreshold rather than a distant parent theorem. That keeps the cost interface uniform with the rest of the monolith (RCL, T5 J-uniqueness) without introducing a second cost functional.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.