用数学构造法高效生成有限域上的自对偶码，并在Lean中形式化验证。
Formalizing building-up constructions of self-dual codes through isotropic lines in Lean
- 通过交错线与双曲几何统一不同构造方法
- 实现5、13元域上最优自对偶码的高效生成
- 适合代数编码与形式化验证研究者
本文有两个目标：首先证明金氏的二元自对偶码构造法等价于Chinburg-Zhang的希尔伯特符号构造法；其次引入q元情形下的Chinburg-Zhang构造，以高效构建q元自对偶码。针对满足q ≡ 1 mod 4的分裂有限域F_q，从构造法、二元算术约化及欧氏平面的双曲几何三个角度进行研究。-1为平方是三者共有的代数基础：在二元情形下对应拉格朗日约化，在分裂q元情形下则决定扩展公式中的修正项。基于高效生成矩阵，我们构造出若干最优自对偶码：如GF(5)上的[6,3,4]和[8,4,4]码，GF(13)上的MDS自对偶[8,4,5]、[10,5,6]码，以及[12,6,6]码。所有结构结论均配有Lean 4的形式化证明。
原文摘要 · Abstract (English)
The purpose of this paper is two-fold. First we show that Kim's building-up construction of binary self-dual codes is equivalent to Chinburg-Zhang's Hilbert symbol construction. Second we introduce a $q$-ary version of Chinburg-Zhang's construction in order to construct $q$-ary self-dual codes efficiently. For the latter, we study self-dual codes over split finite fields \(\F_q\) with \(q \equiv 1 \pmod{4}\) through three complementary viewpoints: the building-up construction, the binary arithmetic reduction of Chinburg--Zhang, and the hyperbolic geometry of the Euclidean plane. The condition that \(-1\) be a square is the common algebraic input linking these viewpoints: in the binary case it underlies the Lagrangian reduction picture, while in the split \(q\)-ary case it produces the isotropic line governing the correction terms in the extension formulas. As an application of our efficient form of generator matrices, we construct optimal self-dual codes from the split boxed construction, including self-dual \([6,3,4]\) and \([8,4,4]\) codes over \(\GF{5}\), MDS self-dual \([8,4,5]\) and \([10,5,6]\) codes over \(\GF{13}\), and a self-dual \([12,6,6]\) code over \(\GF{13}\). These structural statements are accompanied by a Lean~4 formalization of the algebraic core.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。