domainCost
plain-language theorem explainer
Domain cost scores a positive ratio m/e by the RS recognition cost J. Acoustics and RT60 certification code cite it as the scalar mismatch between a measured quantity and a reference scale. The body is a one-line abbreviation of Jcost on the quotient.
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 cost of a positive ratio.
background
The module treats reverberation time RT60 in Recognition Science units: studio targets sit near $\varphi^3\cdot 0.1,\mathrm{s}\approx 0.424,\mathrm{s}$, with concert-hall scales near $\varphi^5\cdot 0.1,\mathrm{s}$. Status is structural (no sorry, no axioms).
The unique cost forced by the Recognition Composition Law is $J(x)=\frac12(x+x^{-1})-1$ for $x>0$. Upstream docs call this "the RS recognition cost of a positive ratio" and note that any genuine distinction (ratio not one) has strictly positive cost. Domain cost simply feeds the quotient $m/e$ into that functional, so a matched pair costs zero and a mismatch costs the usual hyperbolic defect.
proof idea
Pure definition: expand as the existing J-cost applied to the ratio $m/e$. No tactics, no lemmas beyond the imported Jcost abbreviation.
why it matters
Gives the acoustics layer a uniform scalar for how far a measured level sits from a reference energy or time scale, using the same J forced at T5 in the unified forcing chain. Sibling lemmas (non-negativity, value at equality, canonical threshold, RT60Cert) build certificates on top of this score. No downstream edges are recorded yet; the definition is the local hook that lets RT60 claims speak the global cost language rather than an ad-hoc residual.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.