domainCost
plain-language theorem explainer
Domain cost of two real quantities is the recognition cost of their ratio. Acoustics and ladder-matching arguments cite it when comparing a measured frequency scale to an RS energy or yardstick scale. The body is a one-line abbreviation: apply the standard J-cost to m/e.
Claim. For real numbers $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
Recognition Science measures mismatch of positive scales by the J-cost $J(x)=\frac{x+x^{-1}}{2}-1$. Upstream definitions state this is the unique cost forced by the Recognition Composition Law, and that a genuine distinction (ratio not one) has strictly positive cost. The same formula appears across Cost, Cosmology, Gravity, and Spiral modules.
This module sits in the acoustics lane: middle C at 261.63 Hz is compared to a phi-ladder frequency of the form $\varphi^{14}$ times a dimensionless factor near 0.31, giving about 261.3 Hz. Domain cost packages the ratio of a measured scale $m$ to a reference energy or yardstick $e$ so later lemmas can talk about nonnegativity and thresholds without rewriting $J$ each time.
proof idea
Pure definitional abbreviation. No tactics: the value is exactly Jcost (m / e), with Jcost the standard noncomputable cost $(x+x^{-1})/2-1$ imported from the Cost stack.
why it matters
Gives the acoustics module a named cost on frequency or mass-energy ratios before proving nonnegativity (domainCost_nonneg), evaluation identities (domainCost_at_eq), and the middle-C certificate (MiddleCFreqRS, cert). It ties the empirical 261.63 Hz match to the same J forced at T5 in the unified forcing chain and used for phi-ladder mass and frequency claims elsewhere. No downstream edges are recorded yet; siblings in-module are the immediate consumers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.