domainCost_nonneg
plain-language theorem explainer
The domain cost of two positive reals is nonnegative. Acoustics work on the RS A4 (440 Hz) exactness certificate cites this positivity fact. Proof is a one-line unfold of domain cost into J-cost of the ratio, then the standard AM-GM nonnegativity of J.
Claim. For all real $m>0$ and $e>0$, the domain cost of $m$ relative to $e$ (the Recognition $J$-cost of the ratio $m/e$) is nonnegative: $0\le J(m/e)$.
background
Recognition Science measures mismatch with the cost $J(x)=(x+x^{-1})/2-1$ for $x>0$. Equivalently $J(x)=(x-1)^2/(2x)$; nonnegativity is AM-GM (or a direct square). Upstream lemmas record $J(x)\ge 0$ whenever $x>0$.
This module treats the ISO A4 standard (440 Hz) against the phi-ladder prediction $\phi^{17}\cdot 0.123\approx 439.2$ Hz. Domain cost is the local name for $J$ applied to a positive frequency (or scale) ratio $m/e$, so positivity is the first structural fact needed before thresholds or certificates.
proof idea
One-line wrapper. Unfold the definition of domain cost (which is $J$ of the ratio). The hypotheses $m>0$ and $e>0$ give $m/e>0$ by div_pos. Finish by applying the upstream lemma Jcost_nonneg to that positive quotient.
why it matters
Local positivity lemma inside the acoustics A4 exact-RS development (structural, zero sorry). It underwrites any later comparison of measured pitch scales to the phi-ladder yardstick near 440 Hz. No downstream dependents are wired yet; the lemma sits beside domainCost, the canonical threshold, and the A4 certificate inhabitants. Framework link: T5 J-uniqueness forces this same $J$, so nonnegativity is inherited from the forcing chain rather than postulated ad hoc for music.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.