srCost_pos_off_threshold
plain-language theorem explainer
Speech-recognition cost on the signal-to-noise ratio is strictly positive for any positive ratio not equal to one. Acousticians and audiologists modeling intelligibility thresholds would cite this to bound penalties away from the recognition threshold. The proof is a direct one-line application of the general J-cost positivity lemma.
Claim. For any real number $r > 0$ with $r ≠ 1$, the speech-recognition cost satisfies $0 < srCost(r)$.
background
The module shows speech intelligibility governed by recognition cost on the SNR ratio $r$ defined as signal power over noise power. The intelligibility-1 condition holds at $r = 1$ with zero J-cost; below this, J-cost rises and intelligibility drops. The clinical analog is the speech-reception threshold at roughly -7 dB, corresponding to $r ≈ 0.2$ for healthy listeners.
proof idea
The proof is a one-line wrapper that applies the lemma Jcost_pos_of_ne_one from the Cost module directly to the definition of srCost.
why it matters
This result confirms strict positivity of speech-recognition cost off the recognition threshold and supports the hearing-loss penalty constructions in the same module. It instantiates J-cost positivity at the SNR level, consistent with the Recognition Science forcing chain and the definition of J-cost as the quadratic form that vanishes only at unity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.