domainCost
plain-language theorem explainer
Domain cost scores a pair of real scales by the recognition cost of their ratio. RS ecology work cites it when measuring how far a mass-like versus energy-like balance sits from unit parity. The body is a one-line specialization of the unique J-cost functional to m/e.
Claim. For real numbers $m$ and $e$, define the domain cost by $J(m/e)$, where $J(x)=\frac{x+x^{-1}}{2}-1$ is the recognition cost of a positive ratio.
background
The Ecology module frames biotic interaction types (competition, mutualism, predation, amensalism, commensalism) as the five axes of recognition configuration space, matching configDim $D=5$. Status is structural: zero sorry, zero axiom.
The underlying cost is the RS J-functional $J(x)=\frac{x+x^{-1}}{2}-1$, forced uniquely by the Recognition Composition Law (T5). Upstream copies state the same formula and record that a genuine distinction (ratio not one) has strictly positive cost, and that $J$ is nonnegative on positive reals.
Domain cost simply feeds the ratio of two real parameters into that functional. In the ecology setting those parameters are read as mass-like and energy-like scales whose imbalance measures departure from balanced recognition.
proof idea
Pure definition: one-line abbreviation that applies the imported J-cost functional to the quotient $m/e$. No tactics, no lemmas, no proof obligations.
why it matters
Gives the Ecology module a named cost on domain ratios so later certificates (nonnegativity, evaluation at equality, canonical thresholds, biotic-interaction certificates among the siblings) can talk about imbalance without reopening the J formula. It sits under the structural claim that the five classical biotic interaction types equal configDim $D=5$ in recognition space. The definition inherits uniqueness of $J$ from the forcing chain (T5) and the Recognition Composition Law; it does not itself advance T6–T8 or the mass ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.