domainCost
plain-language theorem explainer
Domain cost assigns to a magnitude–energy pair the recognition cost of their ratio. Anyone comparing measured total harmonic distortion against RS audibility thresholds uses this as the local cost map. It is a one-line abbreviation of the standard J-cost evaluated at m/e.
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 total harmonic distortion (THD) in Recognition Science units. Empirically, audible THD sits near 0.5–1%. The RS proposal is that the audible threshold is not bare $J(\varphi)$ (about 11.8%, too high) but $J(\varphi)^{D-1}=J(\varphi)^2\approx 1.39%$, matching the ~1% band once spatial dimension $D=3$ is inserted.
The cost functional is the unique J forced by the Recognition Composition Law: $J(x)=\frac12(x+x^{-1})-1$ for $x>0$. Upstream modules (Cost, CoherenceCollapse, EnergyProcessingBridge, and others) all expose the same definition; a genuine distinction (ratio not one) has strictly positive cost. Domain cost simply specializes that functional to the acoustics ratio of magnitude to energy.
proof idea
Pure definitional abbreviation: domain cost of $(m,e)$ is defined to be $J(m/e)$. No proof obligations; the body is the single application of the imported J-cost.
why it matters
Gives the acoustics module a named cost on the magnitude–energy ratio so later certificates (non-negativity, value at equality, canonical threshold, and the inhabited HarmonicDistCert) can speak in domain language rather than raw J. Ties the THD audibility claim to the forcing-chain landmarks: T5 J-uniqueness and T8 $D=3$, which together justify the squared factor $J(\varphi)^2$ in the module header. No downstream consumers are wired yet; the definition is the local entry point for that structural theorem chain (0 sorry, 0 axiom).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.