srCost_nonneg
plain-language theorem explainer
The speech-recognition cost srCost(r), defined as the J-cost on signal-to-noise ratio r, is non-negative whenever r exceeds zero. Acoustics modelers working with intelligibility thresholds would cite this to confirm that recognition penalties cannot become negative. The proof is a one-line wrapper that invokes the established non-negativity lemma for Jcost.
Claim. For every positive real number $r$, the speech-recognition cost on the signal-to-noise ratio satisfies $srCost(r) := J(r) ≥ 0$, where $J$ denotes the J-cost function.
background
The module models speech intelligibility via recognition cost on the ratio $r$ = signal power over noise power. It defines $srCost(r) := Cost.Jcost r$, where Jcost is the standard J function $J(x) = (x + x^{-1})/2 - 1$. The module documentation notes that intelligibility reaches its peak at $r = 1$ (zero J-cost) and declines as $r$ falls below this value, with clinical SRT values around $r ≈ 0.2$.
proof idea
The proof is a one-line wrapper that applies the lemma Cost.Jcost_nonneg to the hypothesis $hr : 0 < r$. Because srCost is definitionally equal to Jcost, the non-negativity statement transfers directly without further steps.
why it matters
This result supplies the cost_nonneg field inside the SpeechIntelligibilityCert structure that aggregates the core properties of srCost. It confirms that the J-cost framework, introduced at the T5 J-uniqueness step of the forcing chain, yields non-negative penalties when applied to acoustics, thereby supporting downstream derivations of reciprocal symmetry and hearing-loss penalties.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.