speechIntelligibilityCert
plain-language theorem explainer
Speech intelligibility is modeled via J-cost on signal-to-noise ratio r, with the certificate asserting that this cost vanishes at r=1, is symmetric under inversion, nonnegative for r>0, and that hearing-loss penalties vanish at zero rungs while remaining nonnegative. Acousticians deriving word-recognition scores from SNR would cite the structure. The definition assembles the certificate by direct substitution of the five sibling theorems on srCost and hearingLossPenalty.
Claim. The speech-intelligibility-from-J-cost certificate is the structure asserting that the recognition cost on signal-to-noise ratio satisfies $srCost(1)=0$, $srCost(r)=srCost(r^{-1})$ for all $r>0$, $srCost(r)≥0$ for all $r>0$, the hearing-loss penalty vanishes at zero rungs, and is nonnegative for every natural number of rungs.
background
In the Recognition Science acoustics module, speech intelligibility is governed by recognition cost applied to the signal-to-noise ratio r measured in relevant frequency bands. The module defines srCost as the J-cost function on r and hearingLossPenalty as the additive cost for k rungs of impairment. Upstream theorems establish that srCost vanishes at unity (Cost.Jcost_unit0), is symmetric under inversion (Cost.Jcost_symm), and nonnegative (Cost.Jcost_nonneg), while the penalty is zero at k=0 and nonnegative at every rung.
proof idea
The definition constructs the SpeechIntelligibilityCert structure by supplying its five fields directly from sibling results: srCost_zero_at_threshold supplies threshold_zero, srCost_reciprocal_symm supplies reciprocal_symm, srCost_nonneg supplies cost_nonneg, hearingLossPenalty_zero supplies penalty_zero, and hearingLossPenalty_nonneg supplies penalty_nonneg.
why it matters
This certificate supplies the formal link between J-cost and speech intelligibility, grounding clinical SRT shifts in the phi-ladder of recognition cost. It closes the acoustics application of the core Cost properties and is consistent with T5 J-uniqueness and the eight-tick octave. No downstream uses are recorded, leaving open the derivation of explicit word-recognition curves from the certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.