Lean 4 Formalization of Contraction Coefficients for Jensen-Shannon Divergence

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_mean_remainder_bound` for closing lemma1_local_jsd_metric. **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)