domainCost
plain-language theorem explainer
Domain cost assigns the RS recognition cost of a measured-versus-expected ratio: J(measured/expected). Acoustics and room-acoustics derivations cite it when folding impulse-response or absorption data into the J-cost calculus. The body is a one-line definition that applies the standard J-cost to that ratio.
Claim. For real numbers $m$ (measured) and $e$ (expected), 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 room impulse response in Recognition Science units. Its structural claim is that reverberation time obeys the Sabine-type law $T_{60}=0.161,V/(A\alpha)$ with the canonical absorption near the diffuse-field optimum satisfying $\alpha\approx J(\varphi)$.
The cost functional is the unique J forced by the Recognition Composition Law: $J(x)=\frac{1}{2}(x+x^{-1})-1$ (equivalently $\cosh(\log x)-1$). Upstream docs state it is the RS recognition cost of a positive ratio, nonnegative for $x>0$, and strictly positive when the ratio is not one. Domain cost simply evaluates that functional on a measured/expected ratio, so equilibrium (ratio one) is the zero-cost point.
proof idea
Pure definition: no proof obligations. The right-hand side is the shared Jcost from Cost (and re-exports), applied to the quotient of the two real arguments. Downstream lemmas in the same file (nonnegativity, equilibrium vanishing) inherit the corresponding properties of J.
why it matters
Gives the acoustics module a single named map from empirical ratios into the RS cost lattice, so room-impulse certificates can speak the same language as the forcing chain (T5 J-uniqueness) and the RCL. Siblings build on it: equilibrium cost zero, nonnegativity, a canonical positive threshold, and the RoomImpulseCert package that ties absorption to $J(\varphi)$. That links classical RT60 bookkeeping to the phi-ladder cost geometry without new axioms. No external used-by edges yet; the immediate consumers are the in-module cert constructors.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.