domainCost
plain-language theorem explainer
Domain cost assigns the unique Recognition cost J to a mass-to-energy (or measure-to-scale) ratio m/e. Acoustics and phi-ladder frequency work use it when scoring how far a measured pitch sits from an exact RS target. The body is a one-line specialization of the forced cost functional J(x)=(x+x^{-1})/2-1.
Claim. For real $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 the ISO A4 standard (440 Hz) as an RS structural claim: 440 Hz sits near $\varphi^{17}\cdot 0.123\approx 439.2$ Hz, so the pitch is a near-exact rung on the phi ladder. Status is structural (no sorry, no axiom).
The cost functional $J$ is the unique nonnegative functional forced by the Recognition Composition Law: $J(x)=\frac{x+x^{-1}}{2}-1$ (equivalently $\cosh(\log x)-1$). Upstream docs call it "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 ratio of two real parameters into that same $J$.
In this acoustics setting the two arguments are a measured quantity and a reference scale (mass/energy, frequency/yardstick, or analogous pairs). Sibling lemmas then record evaluation identities and nonnegativity before the A4 exactness certificate.
proof idea
Pure definition: one-line abbreviation that applies the global $J$-cost to the quotient $m/e$. No tactics, no lemmas, no side conditions in the body. Downstream facts (evaluation at equality, nonnegativity) are proved separately from the known calculus of $J$.
why it matters
Gives the acoustics module a named cost on frequency or scale ratios so the A4 exactness certificate can score 440 Hz against the phi-ladder prediction without reopening the forcing of $J$. That forcing is T5 in the unified chain: $J$ is the unique solution of the Recognition Composition Law. The module then asks whether the ISO pitch is an exact RS rung ($\varphi^{17}$ times the 0.123 yardstick factor).
No downstream edges are recorded yet; siblings domainCost_nonneg, canonicalThreshold, and A4ExactRS are the intended consumers. The definition is scaffolding-free infrastructure for those structural claims, not a physics derivation by itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.