SpeechIntelligibilityCert
plain-language theorem explainer
Speech intelligibility is modeled by applying J-cost to the signal-to-noise ratio r, producing a cost that vanishes at r=1, remains invariant under r to 1/r, and stays nonnegative. The certificate also bundles a hearing-loss penalty obtained by evaluating the same cost at negative integer powers of phi. Auditory modelers and clinical researchers would cite this structure to certify that a given cost function satisfies the minimal axioms for deriving intelligibility from recognition cost. The declaration is a bare structure definition whose five
Claim. A speech-intelligibility-from-J-cost certificate consists of a cost function $c(r)$ on the positive signal-to-noise ratio $r$ together with a penalty function $p(k)$ on natural numbers $k$ such that $c(1)=0$, $c(r)=c(r^{-1})$ for all $r>0$, $c(r)geq 0$ for all $r>0$, $p(0)=0$, and $p(k)geq 0$ for every natural number $k$.
background
In this module speech intelligibility is obtained by evaluating recognition cost on the ratio $r$ of signal power to noise power in relevant frequency bands. The function srCost is defined as the J-cost applied directly to $r$, while hearingLossPenalty evaluates srCost at $phi^{-k}$ for integer rung $k$ of SNR degradation. The module states that the intelligibility-1 condition holds at $r=1$ with zero cost and records clinical SRT values near $rapprox 0.2$ for healthy listeners, with shifts of one to three phi-rungs for hearing-impaired subjects. Upstream, srCost inherits nonnegativity from the ObserverForcing theorem that the cost of any recognition event is nonnegative, and the cost itself descends from the derivedCost of a multiplicative recognizer comparator.
proof idea
The declaration is a structure definition containing no proof body. Its five fields are instantiated in the downstream construction speechIntelligibilityCert by direct application of the lemmas srCost_zero_at_threshold, srCost_reciprocal_symm, srCost_nonneg, hearingLossPenalty_zero, and hearingLossPenalty_nonneg.
why it matters
The certificate packages the minimal axioms required to derive speech intelligibility scores from J-cost on SNR and is consumed by the speechIntelligibilityCert definition that builds a concrete instance. It links the J-cost (T5) and phi-ladder (T6) of the forcing chain to auditory perception, closing the path from the multiplicative-recognizer cost to clinical metrics without new axioms. The module doc notes that SRT shifts of +5 to +15 dB correspond to one to three rungs of penalty, supplying the concrete bridge between Recognition Science constants and audiology data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.