{"id":"palomar/PALOMAR-2026-09-05-000003","url":"https://github.com/shhyang/n4code_lean/tree/1a501146e430d46c355aa937689f88f24e5ea822","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-05-000003-v1.json","repo":"https://github.com/shhyang/n4code_lean","tags":["cs.IT","math.IT","msc:94B05","coding-theory","lean-formalization","information-theory"],"score":0,"title":"N4Code: optimal finite-length block codes of size four for binary symmetric channels","trust":"high","domain":"cs.IT","source":"palomar","authors":["Shenghao Yang","Yanyan Dong"],"reviews":0,"subject":"cs.IT","summary":"A Lean 4 and mathlib formalization of the Dong-Yang classification of optimal (n,4) binary block codes for binary symmetric channels. The registered results are Theorems 1-5 of the paper: existence of an optimal linear or Class-I code, the explicit linear optimal codes by residue class modulo 3, the universal strict-improvement reductions outside the linear, Class-I, and Class-II classes, the Class-I condition reduction to linear codes, and the finite classification for blocklengths 2 <= n <= 8. The Lean statements use the strict-improvement contrapositive forms.","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"verified":true,"discussed":0,"published":"2026-09-05","reactions":{},"formalized":true,"formalizes":[{"title":"On Optimal Finite-Length Block Codes of Size Four for Binary Symmetric Channels","identifier":"10.1109/TIT.2024.3504823","relationship":"formalizes"}]}