domainCost
plain-language theorem explainer
Domain cost assigns the RS recognition cost J to the ratio of two positive reals m and e. Information theorists working the Shannon-max module cite it when measuring how far a mass-energy pair sits from unit ratio. The body is a one-line abbreviation of Jcost applied to m/e.
Claim. For real numbers $m$ and $e$, the domain cost is $J(m/e)$, where the recognition cost is $J(x)=\frac{x+x^{-1}}{2}-1$.
background
The module treats maximum Shannon entropy for an n-symbol alphabet: $H_{\max}=\log_2 n$ bits. In Recognition Science, when the alphabet size sits on a golden-ratio rung $n=\varphi^k$, this becomes $H_{\max}=k\log_2\varphi\approx k\cdot 0.694$ bits, so phi-rung alphabets maximize information efficiency.
The underlying cost is the unique J-functional forced by the Recognition Composition Law (T5): $J(x)=\frac12(x+x^{-1})-1$, equivalently $\cosh(\log x)-1$. Upstream definitions across Cost, Cosmology, Gravity, and Spiral all fix the same formula and record that a genuine distinction (ratio not one) has strictly positive cost. Domain cost simply specializes that functional to a mass-over-energy ratio.
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 Shannon-entropy-max module a named handle on the RS cost of a mass-energy ratio, so later certificates (nonnegativity, equality at unit ratio, canonical thresholds) can speak in domain language rather than raw J. It sits inside the structural theorem layer of the information domain (0 sorry, 0 axiom) and inherits uniqueness of J from the forcing chain T5 and the Recognition Composition Law. No downstream consumers are wired yet; siblings such as domainCost_nonneg and canonicalThreshold are the immediate consumers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.