domainCost
plain-language theorem explainer
Domain cost assigns to a mass–energy pair the recognition cost of their ratio: J(m/e). It is the local scalar used throughout the RS arrow-of-time module when ledger postings are scored. The definition is a one-line specialization of the unique J-cost forced by the Recognition Composition Law.
Claim. For real $m$ and $e$, the domain cost is $J(m/e)$, where $J(x)=\frac{x+x^{-1}}{2}-1$ is the recognition cost of a positive ratio.
background
The module treats the thermodynamic arrow of time as a statistical irreversibility of ledger postings: J-cost is not time-reversal symmetric in practice, the eight-tick cycle fixes a preferred phase direction, and entropy is J-cost integrated over recognition channels.
The underlying cost is the unique functional $J(x)=\frac12(x+x^{-1})-1$ forced by the Recognition Composition Law (T5). Upstream copies of Jcost state that a genuine distinction (ratio not one) has strictly positive cost and that J is nonnegative for positive arguments. Domain cost simply feeds the mass-to-energy ratio into that functional, so the same algebraic properties apply once $m/e>0$.
proof idea
Pure definitional abbreviation: domainCost m e is defined to be Jcost (m / e). No tactics or lemmas; the body is the single application of the imported J-cost.
why it matters
Supplies the scalar that the arrow-of-time certificate and its siblings (nonnegativity, evaluation at equality, canonical threshold) act on. In the RS forcing chain this is the concrete J of T5 specialized to a mass–energy channel, so entropy bookkeeping and irreversible postings are measured in the same units as the rest of the monolith. No downstream users are recorded yet; the definition exists to keep the module’s later structural theorems free of inline Jcost (m/e) noise.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.