srCost_zero_at_threshold
plain-language theorem explainer
The theorem fixes the speech-recognition J-cost to zero exactly at signal-to-noise ratio unity. Auditory modelers working with Recognition Science cost functions would cite it to anchor the maximum-intelligibility threshold. The proof is a direct one-line reduction to the underlying J-cost unit lemma.
Claim. Let $J(r)$ denote the J-cost applied to signal-to-noise ratio $r$. Then $J(1)=0$.
background
The module models speech intelligibility via J-cost on the signal-to-noise ratio $r$ in frequency bands, with the intelligibility-1 condition at $r=1$. The sibling definition sets srCost$(r)$ to the core J-cost function. The upstream Jcost_unit0 lemma states Jcost 1 = 0 by simplification of the squared-ratio form $J(x)=(x-1)^2/(2x)$.
proof idea
The proof is a one-line wrapper that applies the Jcost_unit0 lemma from the Cost module directly to the definition of srCost.
why it matters
This supplies the threshold_zero field inside the SpeechIntelligibilityCert structure that assembles the full set of intelligibility properties. It embeds the core J-cost zero point into the acoustics application, consistent with J-uniqueness and the Recognition Composition Law. The module carries zero sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.