通过各向异性线在Lean中形式化构建自对偶码的构造
信息论
2026-04-10 v1 计算与语言
math.IT
摘要
本文有两个目标。首先，我们展示了Kim的二进制自对偶码的构建-上构造等价于Chinburg-Zhang的Hilbert符号构造。其次，我们引入了Chinburg-Zhang构造的q进制版本，以有效地构造q进制自对偶码。对于后者，我们通过三个互补视角来研究q进制自对偶码，其中q满足q≡1（mod 4），包括构建-上构造、Chinburg-Zhang的二进制算术简化，以及欧几里得平面的双曲几何。使-1为完全平方的条件是这些视角之间的公共代数输入：在二进制情况下，它构成Lagrangian归约图的基础，而在分裂q进制情况下，它产生支配校正项的各向异性线，从而控制扩展公式。作为应用，我们利用高效的生成矩阵形式，从分裂盒子构造中构建最优自对偶码，包括GF(5)上的[6,3,4]和[8,4,4]自对偶码，GF(13)上的MDS自对偶[8,4,5]和[10,5,6]码，以及GF(13)上的[12,6,6]自对偶码。这些结构声明伴随Lean 4形式化的代数核心。
引用
@article{arxiv.2604.08485,
title = {Formalizing building-up constructions of self-dual codes through isotropic lines in Lean},
author = {Jae-Hyun Baek and Jon-Lark Kim},
journal= {arXiv preprint arXiv:2604.08485},
year = {2026}
}
备注
27 pages