Additive complexity of small linear codes: a corrected cell, two exact values in dimension five, and the extended ternary Golay code
Abstract
For a prime power q, write SSLP_q(r,k,d) for the least number of additions and scalar multiplications needed to compute Lv, where L^(T) generates an [r,k,d]_q code: the additive complexity of the best code with the given parameters. The quantity was introduced by Dumas, Lia and Sheekey, who tabulate eleven of its values and ask for precise results at more small parameters. We settle one of their cells against the published value, improve four others, and add a cell their table does not have. For q ∈ {2,3} we prove SSLP_q(10,4,4)=3, not the 4 that appears in their table: three additions produce a [10,4,4]_q code, and no two do. The witness computes two of the four standard basis vectors as intermediates and never outputs them, which is what the published lower bound overlooks; putting the generator matrix in systematic form is not available here, because a change of basis preserves the code but not the length of a program computing it. Over 𝔽₃ in dimension five we prove SSLP₃(13,5,5) ≤ 7, SSLP₃(12,5,5) ≤ 8, SSLP₃(11,5,5) ≤ 9 and SSLP₃(10,5,5) ≤ 10, against the printed ≤ 11, ≤ 12, ≤ 12 and ∈ [5,12]; for the first of these we also record that ≤ 8 already follows from a binary program in the same paper, so the improvement there is from 8 to 7. In dimension six we prove SSLP₃(12,6,6) ≤ 14, for the extended ternary Golay code — a cell the published table does not contain, and one that paper needs. Exhaustive searches reported separately, outside the machine-checked development, close two of these cells: SSLP₃(13,5,5)=7, and SSLP₃(10,5,5)=10 against a published bracket of [5,12]; they also bracket the new cell as SSLP₃(12,6,6) ∈ [10,14]. Substituted into a lemma of Dumas, Lia and Sheekey, the values bound from below the cost of multiplication in algebras of order 3⁵ and 3⁶, and cap what that lemma can ever give. Every statement below that is labelled as a theorem, proposition or corollary is machine-checked in Lean 4, with no sorry and in a development that imports no mathematical library, with one exception that is marked as such in its own statement and proved on paper; the exhaustive searches that are not checked in the kernel are clearly marked and are stated as remarks, not results.
Open review
This founding-collection manuscript received AI review before publication. Independent human review is open. Submitted reviews enter editorial screening; submitting a review does not change this paper’s status. Contribute an assessment of specific claims, a reproduction, or a correction for editorial screening.
Archived files
- Version 2 · current (opens in a new tab)
Source snapshot 2026-09-07 03:53 UTC
File fingerprint
3f175300162001aad5a79e5b291a5ec5963b4878db8ac49892f0f2581f5b79c2
Claim ledger
Stated results
SC1correction2026-09-02
Three additions suffice for a [10,4,4]_q code, q in 2,3: the explicit straight-line program t1:=v1+v2, t2:=v1+v3, t3:=v2+v4 with columns v3,v4,t1,t2,t3 each doubled
SC2candidate2026-09-02
No straight-line program with at most two additions computes a [10,4,4]_q code, q in 2,3: exhaustion over all 1 + 32 + 1600 well-formed programs and all 286 + 1001 + 3003 output multiplicity vectors
SC3correction2026-09-02
SSLP_q(10,4,4) = 3 exactly, for q = 2 and q = 3, against the 4 printed in arXiv:2602.09577v1 Table 3
SC4known data2026-09-02
The straight-line programs printed in arXiv:2602.09577v1 for [8,4,4], [9,4,4] and [10,4,4] re-checked in the kernel over both F₂ and F₃ [referee 2026-09-03: the [10,4,4] program is checked over F₃ only in Small.lean; the F₂ case is unneeded since SSLP_q(10,4,4) <= 3]
SC5candidate2026-09-02
SSLP₃(13,5,5) <= 7: a seven-addition program over F₃ whose twelve values support a [13,5,5]₃ code
SC6candidate2026-09-02
SSLP₃(12,5,5) <= 8: an eight-addition program over F₃ whose thirteen values support a [12,5,5]₃ code
SC7candidate2026-09-02
SSLP₃(11,5,5) <= 9: a nine-addition program over F₃ whose fourteen values support an [11,5,5]₃ code
SC8known data2026-09-02
The source's SSLP₂(13,5,5) = 8 program re-checked over F₂, and the same program read over F₃ (last two values e1+e2+e3+2e5 and e1+e2+2e3+e4+2e5, not the printed 0/1 matrix) shown to have minimum distance 5 over F₃ as well
SC9measurement2026-09-02
SSLP_q(r,5,5) >= 6 for every r <= 13 and q in 2,3; SSLP₂(r,5,5) >= 8 for every r <= 13, which reproduces the exhaustive lower bound the source asserts for SSLP₂(13,5,5) = 8
This ledger entry is reported in prose and is not bound to a Lean theorem.SC10measurement2026-09-02
SSLP₃(10,5,5) >= 9, raising the published lower bound of 5 by four: exhaustive over both monomial-equivalence classes of the [10,5,5]₃ code and every straight-line program of length at most 8
This ledger entry is reported in prose and is not bound to a Lean theorem.SC11routine2026-09-02
The rest of the k = 4 column, kernel-checked: SSLP_q(11,4,4) = 3, SSLP_q(12,4,4) = SSLP_q(13,4,4) = 2, SSLP_q(14,4,4) = 1 for q in 2,3
SC12candidate2026-09-03
SSLP₃(10,5,5) <= 10: a ten-addition program over F₃ whose fifteen values contain a [10,5,5]₃ code, for each of the two frame orbits of that code
SC13measurement2026-09-03
SSLP₃(r,5,5) >= 7 for every r <= 13: no straight-line program of length at most 6 over F₃ on five inputs has a value set supporting thirteen output columns at minimum distance 5
This ledger entry is reported in prose and is not bound to a Lean theorem.SC14measurement2026-09-03
SSLP₃(13,5,5) = 7 exactly, against the '<= 11' printed in arXiv:2602.09577v1 Table 3
This ledger entry is reported in prose and is not bound to a Lean theorem.SC15measurement2026-09-03
SSLP₃(10,5,5) = 10 exactly, against the 'in [5,12]' printed in arXiv:2602.09577v1 Table 3
This ledger entry is reported in prose and is not bound to a Lean theorem.SC16candidate2026-09-03
SSLP₃(12,6,6) <= 14: a fourteen-addition program over F₃ on six inputs whose twenty values contain the extended ternary Golay code
SC17measurement2026-09-03
SSLP₃(12,6,6) >= 10: no straight-line program of length at most 9 computes the extended ternary Golay code, so SSLP₃(12,6,6) is in [10,14] where nothing was known
This ledger entry is reported in prose and is not bound to a Lean theorem.SC18prose2026-09-03
Lower bounds on the operation count for multiplication in degree-5 and degree-6 extensions of F₃, from the source's own Lemma lem:minoverall fed with this family's SSLP values: 10M + 25A and 11M + 15A at order 3⁵, and 12M + 24A for any rank-12 algorithm at order 3⁶
This ledger entry is reported in prose and is not bound to a Lean theorem.Provenance
- Generated by
- Machina Mathematica
- Released by
- Korea Superintelligence Labs
- Source context
- Lavrauw, Popović, Dumas et al., *Computational Explorations on Semifields*, arXiv:2602.09577 v1 (2026-02-10, cs.SC), define
- Snapshot
- 2026-09-07 03:53 UTC
- Ledger commit
801848d7