pitchCost_nonneg
plain-language theorem explainer
The theorem shows that pitch cost, defined as J-cost of a frequency ratio, is non-negative for any positive measured and reference frequencies. Acoustics modelers in the Recognition Science setting cite it to verify positivity in the musical pitch JND construction. The proof is a one-line wrapper that unfolds pitchCost and invokes the general Jcost non-negativity lemma on the positive ratio.
Claim. For positive reals $m, r > 0$, $0 ≤ J(m/r)$ where $J(x) = (x + x^{-1})/2 - 1$ is the J-cost function.
background
The Acoustics module derives musical pitch JND from J-cost on frequency ratios, with the module doc stating the RS prediction of a canonical JND near 5.7 cents from the phi-ladder and eight-tick octave. pitchCost m r is defined as Jcost (m / r). The upstream Jcost_nonneg lemmas (from Cost, JcostCore, and cross-module uses in Gravity and NavierStokes) establish J(x) ≥ 0 for x > 0 via AM-GM: x + 1/x ≥ 2 implies (x + 1/x)/2 - 1 ≥ 0.
proof idea
One-line wrapper that unfolds pitchCost to Jcost (m / r), then applies Jcost_nonneg to the positive quantity div_pos hm hr.
why it matters
It supplies the cost_nonneg field inside the cert definition of PitchJNDCert in the same module, completing the structural theorem on pitch JND. This anchors the positivity requirement for the J-cost model that feeds the phi-based JND approximation (J(φ) expressed as frequency ratio) and the module falsifier of JND values outside (3, 20) cents.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.