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 local cost primitive for the RS compression-ratio development, where structured data at $\varphi$-rung complexity is claimed to compress by $J(\varphi)^{-1}\approx 8.47$. The body is a one-line alias of the standard $J$-cost on the quotient.
Claim. For real numbers $m$ and $e$, define the domain cost by $\mathrm{domainCost}(m,e) := J(m/e)$, where $J(x) = \frac{x+x^{-1}}{2}-1$ is the recognition cost of a positive ratio.
background
The module treats maximum lossless compression in Recognition Science terms: the Kolmogorov limit is identified with the reciprocal of the $J$-cost at the golden ratio, $J(\varphi)^{-1}\approx 8.47$ for structured $\varphi$-rung data, versus $1\times$ for random (incompressible) data.
The cost functional is the unique $J$ forced by the Recognition Composition Law (forcing chain T5): $J(x)=\frac{x+x^{-1}}{2}-1$, equivalently $\cosh(\log x)-1$. Upstream copies of $J$ (Cost, CoherenceCollapse, EnergyProcessingBridge, etc.) all use this same formula; EnergyProcessingBridge notes it is the unique cost forced by RCL. Domain cost simply evaluates that functional on the ratio $m/e$, the natural dimensionless argument for a compression or measure-to-encoding comparison.
proof idea
Pure definitional abbreviation: the body is the single term $J(m/e)$ with no proof obligations, tactics, or lemmas. Non-negativity, special values, and threshold comparisons live in sibling lemmas (domainCost_nonneg, domainCost_at_eq, canonicalThreshold).
why it matters
Gives the module a named cost on message/encoding (or measure/energy) pairs so compression certificates can quote a single symbol rather than raw $J$. It sits under the structural compression-ratio claim of the module (status: structural theorem, zero sorry) and inherits uniqueness of $J$ from T5 and the RCL. Downstream siblings build non-negativity, the canonical threshold, and CompressionRatioCert; this def is the shared numeric core. No used-by edges are recorded yet, so its role is local scaffolding for those certificates rather than a cross-module bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.