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

Alex B. Shvets

doi:10.5281/zenodo.18281785

January 17, 2026Open Access

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

View Full Paper

Ask AI

Bookmark

Share

Key Points

The aim is to formalize definitions and theorems related to Jensen-Shannon divergence contraction coefficients in Lean 4.
Utilized Lean 4 for formal verification of mathematical definitions.
Incorporated Mathlib for supporting mathematical libraries.
Defined key parameters: s_m, λ_m, η_JSD, and η_χ².
Established and verified theorems for binary equality and the BSC formula.
Confirmed exact formulas for contraction coefficients using formal methods.
Validated the binary equality case for m=2.
Reinforced m-ary symmetric channel formula with formal proofs.

Implication

Machine-verified formalization demonstrates key theorems on JSD contraction coefficients, suggesting robust definitions in mathematical contexts.

Abstract

Machine-verified formalization of exact formulas for Jensen-Shannon divergence contraction coefficients in Lean 4 with Mathlib. Includes definitions of s_m, λ_m, η_JSD, η_χ², and verified theorems: binary equality (m=2 case), BSC formula, m-ary symmetric channel formula.

Discussion

No takes yet. Share an insight, caveat, or question.

Cite This Study

Alex B. Shvets (2026) studied this question.

synapsesocial.com/papers/696f1ac19e64f732b51ef0ae https://doi.org/10.5281/zenodo.18281785

View Full Paper

Ask AI

Bookmark

Share

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

Key Points

Implication

Abstract

Discussion

Cite This Study

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

Key Points

Implication

Abstract

Discussion

Cite This Study

Keep reading

Keep reading