pith. sign in

arxiv: 2604.08485 · v1 · submitted 2026-04-09 · 💻 cs.IT · cs.CL· math.IT

Formalizing building-up constructions of self-dual codes through isotropic lines in Lean

Jae-Hyun Baek , Jon-Lark Kim This is my paper

Pith reviewed 2026-05-10 16:49 UTC · model grok-4.3

classification 💻 cs.IT cs.CLmath.IT
keywords self-dual codesbuilding-up constructionHilbert symbolisotropic linesfinite fieldsoptimal codesMDS codesLean formalization
0
0 comments X

The pith

Kim's building-up construction of binary self-dual codes is equivalent to Chinburg-Zhang's Hilbert symbol construction.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper establishes that Kim's building-up method for binary self-dual codes produces exactly the same codes as Chinburg and Zhang's construction based on Hilbert symbols. It then defines a q-ary analog that works over finite fields of order congruent to 1 modulo 4 and uses this to build several optimal self-dual codes. The equivalence and the new construction are studied through three linked viewpoints whose common requirement is that minus one is a square in the field. The algebraic identities at the core are verified by a Lean 4 formalization.

Core claim

Kim's building-up construction of binary self-dual codes is equivalent to Chinburg-Zhang's Hilbert symbol construction. A q-ary version over split finite fields F_q with q ≡ 1 mod 4 constructs optimal self-dual codes, including [6,3,4] and [8,4,4] over GF(5) and MDS self-dual codes over GF(13), by studying the codes through building-up, binary arithmetic reduction, and hyperbolic geometry, where the isotropic line controls the correction terms; the algebraic core is formalized in Lean 4.

What carries the argument

The isotropic line in the hyperbolic geometry of the Euclidean plane over the split finite field, which governs the correction terms in the code extension formulas and links the building-up, arithmetic-reduction, and geometric viewpoints.

If this is right

  • The two binary constructions may be used interchangeably because they generate identical sets of self-dual codes.
  • The q-ary split boxed construction produces self-dual codes of parameters [6,3,4] and [8,4,4] over GF(5).
  • It also produces MDS self-dual codes [8,4,5] and [10,5,6] over GF(13) together with a self-dual [12,6,6] code over the same field.
  • The Lean formalization supplies machine-checked proofs of the algebraic identities used to derive the generator matrices.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The geometric role of the isotropic line may supply a template for constructing self-dual codes in other settings where an analogous square root of minus one exists.
  • The verified algebraic core could be reused to certify generator matrices for additional lengths or fields beyond the examples given in the paper.
  • The unification of constructive, arithmetic, and geometric descriptions may simplify proofs that certain parameter sets admit self-dual codes.

Load-bearing premise

That minus one is a square in the finite field, which is required for the isotropic line to exist and to connect the three viewpoints.

What would settle it

An explicit binary self-dual code that can be produced by one of the two constructions but not the other, or a failure to obtain the listed [6,3,4] or [8,4,4] self-dual codes over GF(5) when the q-ary extension formulas are applied.

read the original abstract

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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 2 minor

Summary. The paper shows that Kim's building-up construction of binary self-dual codes is equivalent to Chinburg-Zhang's Hilbert symbol construction, with the equivalence mediated by isotropic lines under the condition that -1 is a square. It then develops a q-ary generalization over split finite fields F_q (q ≡ 1 mod 4) that unifies the building-up method, binary arithmetic reduction, and hyperbolic geometry of the Euclidean plane, yielding explicit generator matrices. As applications, it constructs optimal self-dual codes including [6,3,4] and [8,4,4] over GF(5) and MDS self-dual codes over GF(13), supported by a Lean 4 formalization of the algebraic core.

Significance. If the results hold, the work provides a unified algebraic-geometric framework for efficient construction of self-dual codes, with the Lean 4 formalization of the algebraic core (including generator-matrix formulas and linking conditions) serving as a machine-checked proof that strengthens verifiability and reproducibility. The explicit optimal-code constructions over GF(5) and GF(13) illustrate practical utility, and the parameter-free nature of the core identities (once the isotropic-line condition is fixed) is a notable strength.

minor comments (2)
  1. The abstract lists concrete code parameters ([6,3,4] over GF(5), MDS examples over GF(13)); the main text should include a brief verification table or explicit generator matrices for at least one of these to allow direct checking against the stated formulas.
  2. The scope of the Lean formalization (which parts of the equivalence and extension formulas are covered) could be stated more explicitly in the introduction or a dedicated section, to clarify what remains informal.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive and accurate summary of our work, including the equivalence result, the q-ary generalization, the explicit optimal-code constructions, and the Lean 4 formalization. The recommendation for minor revision is noted. No specific major comments appear in the report, so we have no points requiring response or revision.

Circularity Check

0 steps flagged

No significant circularity; equivalences and constructions are algebraically self-contained with Lean verification

full rationale

The paper derives the equivalence between Kim's binary building-up construction and Chinburg-Zhang's Hilbert symbol construction by exhibiting explicit algebraic identities and linking three viewpoints (building-up, binary reduction, hyperbolic geometry) via the shared condition that -1 is a square in F_q (q ≡ 1 mod 4). This condition directly produces the isotropic line and correction terms in the generator-matrix formulas. The q-ary extension follows by the same identities applied to split finite fields. All core statements are accompanied by a Lean 4 formalization of the algebraic core, which machine-checks the identities and formulas independently of any fitted data or author-specific ansatz. The listed optimal codes ([6,3,4] and [8,4,4] over GF(5), MDS examples over GF(13)) are presented as direct, explicit outputs of the derived generator matrices rather than separate empirical claims. No derivation step reduces by construction to its own inputs, renames a known result, or relies on a load-bearing self-citation whose content is unverified; the formalization decouples the result from any potential circularity.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The work rests on standard finite-field arithmetic and coding-theory definitions with no fitted parameters or new postulated entities; the key linking assumption is the quadratic residuosity of -1.

axioms (2)
  • domain assumption In finite fields F_q with q ≡ 1 mod 4, -1 is a quadratic residue.
    This condition is invoked as the common algebraic input that produces the isotropic line and links the binary, arithmetic, and geometric viewpoints.
  • standard math Standard definitions and properties of self-dual codes, Hilbert symbols, and generator matrices over finite fields.
    These background results from coding theory and algebra are used without re-derivation.

pith-pipeline@v0.9.0 · 5580 in / 1390 out tokens · 67645 ms · 2026-05-10T16:49:53.920874+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

34 extracted references · 34 canonical work pages

  1. [1]

    The build-up construction of quasi self-dual codes over a non-unital ring,

    A. Alahmadi, A. Altassan, H. Shoaib, A. Alkathiry, A. Bonnecaze, and P. Solé, “The build-up construction of quasi self-dual codes over a non-unital ring,” Journal of Algebra and Its Applications , vol. 21, no. 07, 2250143, 2022. 25

    work page 2022

  2. [2]

    E. F. Assmus, J. D. Key, Designs and Their Codes, Cambridge University Press, 1992, Cambridge Tracts in Mathematics, vol. 103 (Second printing with corrections, 1993)

    work page 1992

  3. [3]

    Designs and self-dual codes with long shadows,

    C. Bachoc and P. Gaborit, “Designs and self-dual codes with long shadows,” J. Combin. Theory Ser. A, vol. 105, no. 1, pp. 15–34, 2004

    work page 2004

  4. [4]

    even unimodular lattices, and invariant rings,

    E. Bannai, S. T. Dougherty, M. Harada, and M. Oura, Type II codes, “even unimodular lattices, and invariant rings,” IEEE Trans. Inf. Theory, vol. 45, no. 4, pp. 1194–1205, 1999

    work page 1999

  5. [5]

    A. R. Calderbank, E. M. Rains, P. M. Shor, and N. J. A. Sloane, Quantum error correction via codes over GF(4), IEEE Trans. Inf. Theory , vol. 44, no. 4, pp. 1369– 1387, 1998

    work page 1998

  6. [6]

    Every binary self-dual code arises from Hilbert symbols,

    T. Chinburg and Y. Zhang, “Every binary self-dual code arises from Hilbert symbols,” Homology, Homotopy Appl. , vol. 14, no. 2, pp. 189–196, 2012

    work page 2012

  7. [7]

    On the enumeration of self-dual codes,

    J. H. Conway and V. Pless, “On the enumeration of self-dual codes,” J. Combin. Theory Ser. A , vol. 28, pp. 26–53, 1980

    work page 1980

  8. [8]

    The binary self-dual codes of length up to 32: A revised enumeration,

    J. H. Conway, V. Pless, and N. J. A. Sloane, “The binary self-dual codes of length up to 32: A revised enumeration,” J. Combin. Theory Ser. A , vol. 60, pp. 183–195, 1992

    work page 1992

  9. [9]

    A new upper bound on the minimal distance of self-dual codes,

    J. H. Conway and N. J. A. Sloane,“A new upper bound on the minimal distance of self-dual codes,” IEEE Trans. Inform. Theory , vol. 36, pp. 1319–1333, Nov. 1990

    work page 1990

  10. [10]

    J. H. Conway, and N. J. A. Sloane, Sphere Packings, Lattices and Groups , 3rd edn. Springer, New York, 1998

    work page 1998

  11. [11]

    Self-dual codes over commutative Frobenius rings,

    S.T. Dougherty, J.-L. Kim, H. Kulosman, H. Liu, “Self-dual codes over commutative Frobenius rings,” Finite Fields Appl. , vol. 16, no. 1, 14-–26, 2010

    work page 2010

  12. [12]

    Error detecting and error correcting codes,

    R. W. Hamming, “Error detecting and error correcting codes,” Bell System Technical Journal, vol. 29, no. 2, pp. 147–160, 1950

    work page 1950

  13. [13]

    Singly-even self-dual codes and Hadamard matrices,

    M. Harada and V.D. Tonchev, “Singly-even self-dual codes and Hadamard matrices,” Lecture Notes in Computer Science , vol. 948, Springer, New York, 1995, pp. 279–284

    work page 1995

  14. [14]

    W. C. Huffman, J.-L. Kim, Patrick Solé, Concise Encyclopedia of Coding Theory , CRC Press, Taylor & Francis Group, A Chapman & Hall Book, 2021

    work page 2021

  15. [15]

    W. C. Huffman and V. Pless, Fundamentals of Error-Correcting Codes , Cambridge University Press, 2003

    work page 2003

  16. [16]

    W. C. Huffman, Automorphisms ofcodes with applications to extremal doubly even codes oflength 48, IEEE Trans. Inform. Theory , vol. 28, pp. 511–521, 1982

    work page 1982

  17. [17]

    Kaya and B

    A. Kaya and B. Yildiz, Various constructions for self-dual codes over rings and new binary self-dual codes, Discrete Mathematics, vol. 339, no. 2, pp. 460-469, 2016. 26

    work page 2016

  18. [18]

    New extremal self-dual codes of lengths 36, 38, and 58,

    J.-L. Kim, “New extremal self-dual codes of lengths 36, 38, and 58,” IEEE Trans. Inform. Theory, vol. 47, no. 1, pp. 386–393, 2001

    work page 2001

  19. [19]

    Self-dual codes, symmetric matrices, and eigenvectors,

    J.-L. Kim and W.-H. Choi, “Self-dual codes, symmetric matrices, and eigenvectors,” IEEE Access, vol. 9, pp. 104294–104303, 2021

    work page 2021

  20. [20]

    Euclidean and Hermitian self-dual MDS codes over large finite fields

    J.-L. Kim and Y. Lee, “Euclidean and Hermitian self-dual MDS codes over large finite fields. ”J. Combin. Theory Ser. A , vol. 105, no. 1, pp. 79–95, 2004

    work page 2004

  21. [21]

    Self-dual codes using the building-up construction,

    J.-L. Kim and Y. Lee, “Self-dual codes using the building-up construction,” IEEE Int. Symp. Inform. Theory , Seoul, Korea (South), 2009, pp. 2400–2402

    work page 2009

  22. [22]

    Involutions on 3-manifolds and self-dual, binary codes,

    M. Kreck and V. Puppe, “Involutions on 3-manifolds and self-dual, binary codes,” Homology, Homotopy Appl. , vol. 10, no. 2, pp. 139–148, 2008

    work page 2008

  23. [23]

    Self-dual codes over GF(5),

    J. S. Leon, V. Pless, and N. J. A. Sloane, “Self-dual codes over GF(5),” J. Combin. Theory Ser. A , vol. 32, no. 2, pp. 178–194, 1982

    work page 1982

  24. [24]

    Lagrangian and orthogonal splittings, quasitriangular Lie bialgebras and almost complex product structures,

    H. Montani, “Lagrangian and orthogonal splittings, quasitriangular Lie bialgebras and almost complex product structures,” J. Math. Phys. , vol. 64, 053505, 2023

    work page 2023

  25. [25]

    J. S. Milne, Arithmetic duality theorems, 2nd ed., BookSurge Publishing, Charleston, SC, 2006

    work page 2006

  26. [26]

    The number of isotropic subspaces in a finite geometry,

    V. Pless, “The number of isotropic subspaces in a finite geometry,” Atti Accad. Naz. Lincei Rend., vol. 39, pp. 418–421, 1965

    work page 1965

  27. [27]

    Symmetry codes over GF(3) and new five-designs,

    V. Pless, “Symmetry codes over GF(3) and new five-designs,” J. Combin. Theory , vol. 12, 119–-142, 1972

    work page 1972

  28. [28]

    Rains and N

    E. Rains and N. J. A Sloane, Self-dual codes, in: V. S. Pless, W. C. Huffman (Eds.), Handbook of Coding Theory , Elsevier, Amsterdam. The Netherlands. (1998)

    work page 1998

  29. [29]

    Serre, A course in arithmetic , Grad

    J.-P. Serre, A course in arithmetic , Grad. Texts in Math. 7, Springer-Verlag, New York, 1973

    work page 1973

  30. [30]

    A Mathematical Theory of Communication,

    C. Shannon, “A Mathematical Theory of Communication,” Bell System Technical Jour- nal, vol. 27, no. 3, pp. 379–-423, 1948

    work page 1948

  31. [31]

    M. Shi, Y. J. Choie, A. Sharma, and P. Solé, Codes and Modular Forms: A Dictionary , World Scientific, 2020

    work page 2020

  32. [32]

    Extremal self-dual codes from symmetric designs,

    E. Spence, V.D. Tonchev, “Extremal self-dual codes from symmetric designs,” Discrete Math., vol. 110, pp. 265-–268, 1992

    work page 1992

  33. [33]

    Self-orthogonal designs and extremal doubly even codes,

    V. D. Tonchev, “Self-orthogonal designs and extremal doubly even codes,” J. Combin. Theory A , vol. 52, pp. 197-–205, 1989

    work page 1989

  34. [34]

    V. Y. Yorgov, A method for constructing inequivalent self-dual codes with applications to length 56, IEEE Trans. Inform. Theory , vol. 33, pp. 77-–82, 1987. 27

    work page 1987