domainCost
plain-language theorem explainer
Domain cost measures the recognition cost of a message-to-encoding ratio m/e via the forced J-functional. Information theorists working the RS compression bound cite it as the per-symbol overhead beyond Shannon entropy. The definition is a one-line specialization of J to the 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
The module develops optimal data compression from the RS J-cost. Classical Huffman coding sits between $H(X)$ and $H(X)+1$ bits; the RS claim is that optimal RS encoding incurs $J(\varphi)$ bits of overhead per symbol beyond Shannon entropy.
The cost functional is $J(x) = \frac{1}{2}(x + x^{-1}) - 1$, forced uniquely by the Recognition Composition Law (T5). It vanishes only at ratio one and is nonnegative for $x > 0$. Upstream modules (Cost, CoherenceCollapse, EnergyProcessingBridge) all use this same $J$ as the unique cost of a genuine distinction.
Here $m$ and $e$ play the roles of message measure and encoding measure; their ratio is the natural argument of $J$ when comparing an information domain to its compressed representation.
proof idea
Pure definitional abbreviation: domain cost is exactly $J$ evaluated at the ratio $m/e$. No lemmas or tactics; the body is the single application Jcost (m / e).
why it matters
Gives the module a named cost of a message/encoding pair so later lemmas (nonnegativity, evaluation identities, the DataCompr3 certificate) can speak about compression overhead without repeating the ratio. Sits inside the information-domain reading of T5 J-uniqueness: the same functional that forces $\varphi$ and the eight-tick structure also prices how far an encoding departs from the message. Feeds the structural theorem that RS-optimal codes pay $J(\varphi)$ bits per symbol beyond entropy. No downstream edges are recorded yet; siblings domainCost_nonneg and the compression certificate are the immediate consumers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.