domainCost
plain-language theorem explainer
Domain cost assigns to a mass–energy pair the recognition cost of their ratio. Anyone proving Maxwell-demon lower bounds in RS uses this as the local cost on a thermodynamic domain. It is a one-line definition: apply the unique RS cost functional J to m/e.
Claim. For real $m$ and $e$, the domain cost is $J(m/e)$, where $J(x)=\frac{x+x^{-1}}{2}-1$.
background
The module reformulates Maxwell's demon in Recognition Science: a demon cannot drive recognition cost below $J(\varphi)$ per bit processed; information gain equals that quantum times bits erased. The ambient cost is the unique functional forced by the Recognition Composition Law (forcing chain T5):
$$J(x)=\frac{x+x^{-1}}{2}-1=\cosh(\log x)-1.$$
Upstream modules define the same $J$ (Cost, CoherenceCollapse, EnergyProcessingBridge, SpiralField, RefineTrigger). Domain cost specializes it to a mass-to-energy ratio on a thermodynamic domain, the natural argument when tracking how a sorting demon moves energy relative to mass scale.
proof idea
Pure definitional abbreviation. The body is the single application Jcost (m / e); no tactics, no lemmas, no side conditions at the definition site. Nonnegativity and evaluation identities live in sibling lemmas.
why it matters
Gives the module its working cost on domains so later certificates can state the demon bound in RS units. Siblings (domainCost_nonneg, domainCost_at_eq, canonicalThreshold, MaxwellDemon2DeepCert) build the structural theorem advertised in the module doc: demon information gain equals $J(\varphi)$ per bit erased. That threshold is the self-similar fixed point from T6, so the definition sits on the T5–T6 forcing spine rather than an ad hoc thermodynamic free energy. With zero used_by edges outside the file, its role is local scaffolding for the deep Maxwell-demon certificate in this foundation module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.