domainCost
plain-language theorem explainer
Domain cost assigns to a pair of reals $(m,e)$ the recognition cost of their ratio $m/e$. It is the local cost functional used throughout the RS qubit-channel module when comparing a measured scale against an energy (or reference) scale. Anyone citing the channel-capacity certificate or the nonnegativity lemmas will invoke it. The body is a one-line alias of the unique J-cost.
Claim. For real numbers $m$ and $e$, the domain cost is $J(m/e)$, where $J(x)=\frac{x+x^{-1}}{2}-1$ is the Recognition Science cost of a positive ratio.
background
The module treats qubit channel capacity in Recognition Science units. Classically one qubit carries one bit; RS inserts a recognition overhead so the effective capacity is $\varphi^{-1}$ bits per qubit (about $0.618$). The structural theorems in the file certify that overhead and related positivity statements.
The cost functional $J$ is the unique nonnegative function forced by the Recognition Composition Law: $J(x)=\frac{x+x^{-1}}{2}-1$ (equivalently $\cosh(\log x)-1$). Upstream definitions across Cost, Gravity, Cosmology, and Spiral all fix the same formula and record that a genuine distinction (ratio not one) has strictly positive cost. Domain cost simply evaluates that $J$ on the dimensionless ratio of the two arguments.
proof idea
Pure definitional abbreviation: expand to $J(m/e)$ with the standard $J$-cost. No tactics, no lemmas, no hypotheses.
why it matters
Gives the module a single named cost for scale comparisons that later siblings (nonnegativity, evaluation at equality, canonical threshold, and the qubit-channel certificate) all share. It sits under the T5 J-uniqueness landmark: once $J$ is forced, every channel-capacity overhead statement is just $J$ applied to the right ratio. The module status is structural (zero sorry, zero axiom); this def is the cost primitive those certificates rest on. No downstream edges are recorded yet, so its immediate consumers are the sibling lemmas in the same file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.