domainCost
plain-language theorem explainer
Domain cost assigns to a mass–energy pair the recognition cost of their ratio: J(m/e). Anyone working the RS collapse story (measurement as ledger posting) cites it as the scalar that collapse minimizes toward the nearest rung. The body is a one-line abbreviation of the standard J-cost on the quotient.
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$ (undefined or unconstrained when $e=0$).
background
The module treats wave-function collapse as a recognition event: measurement equals a ledger posting on the eight-tick cycle, with no hidden variables. Collapse is framed as J-cost minimization onto the nearest rung of the phi-ladder.
The upstream cost functional is the unique RS J-cost forced by the Recognition Composition Law and T5: $J(x)=\frac{x+x^{-1}}{2}-1$, also written $\cosh(\log x)-1$. Upstream docs state it is the recognition cost of a positive ratio, strictly positive when the ratio is not one, and nonnegative for positive $x$.
Here $m$ and $e$ are the two real scales whose mismatch the ledger must price; domain cost is simply that price on the ratio $m/e$.
proof idea
Pure definitional abbreviation: apply the imported J-cost to the quotient $m/e$. No tactics, no lemmas, no proof obligations.
why it matters
In the RS collapse picture, the scalar that is minimized is this domain cost. Sibling facts (nonnegativity, evaluation at equality, the canonical threshold, and the collapse certificate) sit on top of it; the module status is structural theorem with zero sorry and zero axiom. It ties the measurement story to the T5 J-uniqueness landmark and to the eight-tick minimal recognition time from the module framing. No downstream dependents are wired yet in the graph, so it is presently a local primitive for the collapse certificate stack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.