srCost_reciprocal_symm
plain-language theorem explainer
The declaration establishes symmetry of speech-recognition J-cost under reciprocal transformation of the signal-to-noise ratio. Acoustics researchers modeling intelligibility thresholds would cite it to justify equal penalties on either side of r = 1. The proof is a one-line wrapper invoking the Jcost symmetry lemma on the srCost definition.
Claim. For every positive real number $r$, the speech-recognition J-cost satisfies $srCost(r) = srCost(r^{-1})$.
background
Speech intelligibility is modeled in this module through the J-cost on the signal-to-noise ratio r defined as signal power divided by noise power. The srCost function is introduced as the direct application of the general J-cost to this ratio. Upstream, the Jcost_symm lemma proves that Jcost(x) equals Jcost of its reciprocal for positive x by field simplification and ring algebra after unfolding the squared expression. The module context notes that intelligibility reaches 50% at r approximately 0.2 for healthy listeners, with shifts for impaired hearing.
proof idea
The proof applies the Jcost_symm lemma from the Cost module, using the hypothesis hr that r is positive, after srCost is identified with Jcost.
why it matters
This supplies the reciprocal symmetry property required by the speechIntelligibilityCert structure, which bundles the J-cost axioms for the acoustics model. It connects to the J-uniqueness step (T5) in the unified forcing chain and ensures consistency with the recognition composition law. The result closes one requirement for the zero-sorry certificate in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.