Lean 4 Formalization of JSD Contraction Coefficients: Core Definitions and Theorems

Zenodo (CERN European Organization for Nuclear Research) 2026 Preprint Open access

Read full text
Authors: Alex B. Shvets
DOI: 10.5281/zenodo.18281784
Cited by: 0

Abstract

Lean 4/Mathlib formalization of JSD contraction coefficients for symmetric channels. Fully verified (no sorry):- Algebraic core: binary equality, strict separation (η_JSD > η_χ² for m≥3), binary uniqueness theorem- Channel definitions: StochChannel structure, BSC, m-ary symmetric channel with verified stochasticity 11 theorems, 9 definitions. ~40% of full theory. First SDPI formalization for JSD. Companion to DOI: 10.5281/zenodo.18039673

Fields of Study & Subjects

Logic programming and type systems Formal Methods in Verification Probability and Statistical Research

Publication details

Journal / source
Zenodo (CERN European Organization for Nuclear Research)
Publication date
17 January 2026
Language
EN
Document type
Preprint