domainCost
plain-language theorem explainer
The domain cost of a mass-energy pair is the recognition cost of their ratio: J(m/e). Anyone working the eight-tick completeness certificate or threshold comparisons cites this abbreviation. It is a one-line definition wrapping the standard J-cost on the positive ratio m/e.
Claim. For real $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 proves that the period-8 lattice covers all $2^D=8$ binary states exactly once per cycle, and that no shorter period does so. That structural fact is the eight-tick completeness theorem (zero sorry, zero axiom).
The underlying cost is the RS recognition functional $J(x)=\frac{x+x^{-1}}{2}-1$, forced uniquely by the Recognition Composition Law (T5). It vanishes only at ratio one and is nonnegative for positive arguments. Domain cost simply evaluates $J$ on the mass-to-energy ratio $m/e$, so that later lemmas can talk about cost of a domain without repeating the quotient.
proof idea
Pure definitional abbreviation: domainCost m e unfolds to Jcost (m / e). No proof obligations.
why it matters
Gives the module a named cost on mass-energy pairs so sibling facts (domainCost_nonneg, domainCost_at_eq, canonicalThreshold) can state nonnegativity and threshold comparisons cleanly. Sits inside the eight-tick completeness development that realizes T7 (period $2^3$) of the forcing chain. No downstream users are recorded yet; the def is local scaffolding for the completeness certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.