Lean 4 Formalization of Contraction Coefficients for Jensen-Shannon Divergence

A Lean 4 formalization of exact formulas for Jensen–Shannon divergence contraction coefficients under symmetric channels. Note (2026). The “binary uniqueness” and “strict inequality” items concern the comparison corrected in the errata to 10.5281/zenodo.18010974 and 10.5281/zenodo.18256326: for channel-only contraction coefficients, ηJSD = ηχ2 for every m. Verified results. Binary uniqueness: m = 2 is the unique case where ηJSD = ηχ2. Strict inequality: ηJSD > ηχ2 for all m ≥ 3. Interior optimality: the supremum is attained at b* ∈ (0, 1). Status. 930+ lines of verified proofs. Three analytic identities are deferred (Taylor expansion, integral representation, SDPI equivalence). Requirements. Lean 4 + Mathlib (January 2026). Reference. A. Shvets, “Contraction Coefficients for Jensen–Shannon Divergence”, 2025, DOI 10.5281/zenodo.18039673.