hearingLossPenalty_nonneg
plain-language theorem explainer
The hearing-loss penalty at rung k equals the J-cost of phi to the power minus k and stays nonnegative for every natural number k. Acoustics researchers modeling speech intelligibility via J-cost on signal-to-noise ratios cite the result to bound penalty increments. The proof unfolds the definition then applies the general J-cost nonnegativity lemma after confirming the argument is positive.
Claim. Let $J$ be the recognition cost. For every natural number $k$, if the hearing-loss penalty equals $J$ evaluated at $phi^{-k}$, then $0 leq J(phi^{-k})$.
background
The module ties speech intelligibility to recognition cost on the signal-to-noise ratio r. The penalty at rung k is defined as the J-cost of phi to the power minus k, where J(x) equals (x plus x inverse) over 2 minus 1. The J-cost is nonnegative for every positive argument by algebraic rearrangement to a square divided by a positive denominator, as shown in the Cost module lemmas.
proof idea
Unfold the penalty definition to expose the J-cost term. Apply the nonnegativity lemma for J-cost. Supply positivity of phi to the power minus k from the positivity of phi.
why it matters
The result is assembled into the speech-intelligibility certificate that collects zero and nonnegativity facts for both base cost and penalty. It confirms penalties remain nonnegative on the phi-ladder, aligning with the recognition composition law. The property closes without new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.