Explicit codewords for fourteen of the twenty-two undetermined weights of the Reed–Muller code RM(7,14)
Abstract
Leuenberger and Albrizzio (arXiv:2606.21425) show that the weight spectrum of the Reed–Muller code RM(7,14) contains every even integer between 312 and 2¹⁴-312, together with the classical small and large weights, with the possible exception of a set M of twenty-two weights, and write that they "were not able to determine the missing weights". We exhibit codewords for fourteen of the twenty-two: a Boolean function of degree 7 in 14 variables with six monomials and Hamming weight 354, functions with between 5 and 19 monomials of weights 8174, 8178, 8182, 8186, 8188, 8190, and their complements of weights 16030, 8210, 8206, 8202, 8198, 8196, 8194. Each codeword is given by its algebraic normal form, and its degree and its weight are checked from the definitions in the kernel of the Lean 4 proof assistant, without any library. We also record a mod 4 law: a codeword of RM(7,14) has weight ≡ 2 (mod 4) exactly when its algebraic normal form contains an odd number of complementary pairs of degree-7 monomials. The remaining four weights 322, 326, 330, 334 (and their complements) were not reached by four independent search families in about 3 · 10⁹ evaluations; we make no claim about their existence. The constructions and tables of the source are reproduced with no discrepancy.
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 1 · current (opens in a new tab)
Source snapshot 2026-09-07 03:53 UTC
File fingerprint
523ef50a9f5a4a7a71328dd06505f8baba13939e830046579c5a967b9f3efb4a
Claim ledger
Stated results
R1known data2026-09-07
Statement description is not included in this imported ledger snapshot. See the PDF for the full theorem wording.
R2known data2026-09-07
Statement description is not included in this imported ledger snapshot. See the PDF for the full theorem wording.
R3candidate2026-09-07
Statement description is not included in this imported ledger snapshot. See the PDF for the full theorem wording.
R4candidate2026-09-07
Statement description is not included in this imported ledger snapshot. See the PDF for the full theorem wording.
R5routine2026-09-07
Statement description is not included in this imported ledger snapshot. See the PDF for the full theorem wording.
R6known data2026-09-07
Statement description is not included in this imported ledger snapshot. See the PDF for the full theorem wording.
R7routine2026-09-07
Statement description is not included in this imported ledger snapshot. See the PDF for the full theorem wording.
R8routine2026-09-07
Statement description is not included in this imported ledger snapshot. See the PDF for the full theorem wording.
R9measurement2026-09-07
Statement description is not included in this imported ledger snapshot. See the PDF for the full theorem wording.
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
- RM(r,m) is the Reed–Muller code of length 2ᵐ whose codewords are the truth tables of the Boolean functions of algebraic degree at most r in m variables. Its weight spectrum is the set of Hamming weights that actually occur. For RM(7,14) the minimum distance is d = 2¹⁴⁻⁷ = 128, the dimension is Σ_(i≤7) C(14,i) = 9908, and the spectrum is not known.
- Snapshot
- 2026-09-07 03:53 UTC
- Ledger commit
801848d7