hearingLossPenalty_zero
plain-language theorem explainer
The hearing-loss penalty vanishes at zero rungs of SNR degradation. Acoustics researchers modeling speech intelligibility via J-cost on signal-to-noise ratios cite this base case to anchor the penalty ladder. The proof is a one-line reduction that unfolds the definition and invokes the unit J-cost lemma.
Claim. Let $P(k)$ be the hearing-loss penalty at rung $k$ of SNR degradation, given by the recognition cost on the phi-scaled ratio. Then $P(0) = 0$.
background
In the acoustics module, speech intelligibility is governed by recognition cost on the signal-to-noise ratio $r$. The hearing-loss penalty at rung $k$ is defined as srCost(phi^{-k}), where srCost applies the J-cost function to the scaled ratio. This captures how intelligibility drops below the $r=1$ threshold, with clinical SRT shifts of +5 to +15 dB corresponding to one to three phi-rungs of penalty. The module states that the intelligibility-1 condition holds at zero J-cost when $r=1$ (Lean status: 0 sorry, 0 axiom). Upstream, the Jcost_unit0 lemma establishes Jcost(1)=0, which supplies the base value for the zero-rung case.
proof idea
The proof unfolds the definition of hearingLossPenalty, reducing the expression to srCost(phi^0) which equals srCost(1). Simplification then applies the Jcost_unit0 lemma directly, which states Jcost(1)=0.
why it matters
This theorem supplies the penalty_zero field inside the SpeechIntelligibilityCert definition, which bundles the core properties (threshold zero, reciprocal symmetry, nonnegativity, and penalty nonnegativity) of the J-cost model for speech recognition. It closes the base case in the acoustics derivation, consistent with the Recognition Science framework where J-cost vanishes at the unit ratio (T5 J-uniqueness). No open questions are touched; the result is a direct consequence of the unit lemma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.