Formal verification of exact formulas for Jensen-Shannon divergence contraction coefficients under symmetric channels. **Verified Results** - **Binary uniqueness**: m=2 is the unique case where ηJSD = η_χ²- **Strict inequality**: ηJSD > η_χ² for all m ≥ 3- **Interior optimality**: Supremum attained at b* ∈ (0, 1) **Files** - `JSDContraction-v2. lean` — Main formalization (930+ lines) - `JSDContraction-Taylor-Lemmas. lean` — Auxiliary lemmas for Taylor expansion (12 lemmas) **Status** Main file: 930+ lines of verified proofs. Three analytic identities deferred (Taylor expansion, integral representation, SDPI equivalence). Taylor lemmas file: 12 verified lemmas establishing derivatives of x·log (x) up to third order, smoothness properties, and norm bounds for iteratedDerivWithin. These prepare the application of `taylorₘeanᵣemainderbound` for closing lemma1ₗocalⱼsdₘetric. **Requirements** Lean 4 + Mathlib (January 2026) **Reference** A. Shvets, *"Contraction Coefficients for Jensen-Shannon Divergence"*, 2025 DOI: 10. 5281/zenodo. 18039673 (https: //doi. org/10. 5281/zenodo. 18039673)
Alex B. Shvets (Tue,) studied this question.