Problem. Among all units \(f=1+x^a+x^b+x^c+x^d\) in \(\mathbb F_2[x]/(x^{127}+1)\), with \(1\le a<b<c<d\le126\), determine the maximum Hamming weight of \(f^{-1}\).
Current status (The maximum inverse weight lies between 85 and 101). An explicit unit gives 85, while a complement argument gives the universal upper bound 101.
1Packet records
6 records
Record
Kind
Assessment
An explicit unit gives 85, while a complement argument gives the universal upper bound 101.
Result
Evidence: Reproduced
A replay is recorded for this computation. Inspect the replay record for its procedure and scope.
claim · Computation 1
An explicit unit gives 85, while a complement argument gives the universal upper bound 101.
Relevance to this problem
For Densest inverse of a weight-five binary cyclic polynomial, record wfci127-claim-certified-interval (“The maximum inverse weight lies between 85 and 101”) records a bound, answer, status fact, or structural consequence. The record states: An explicit unit gives 85, while a complement argument gives the universal upper bound 101.
Evidence
ReproducedA replay is recorded for this computation. Inspect the replay record for its procedure and scope.
Record state
supported
Scope
all normalized weight-five residues 1+x^a+x^b+x^c+x^d in F_2[x]/(x^127+1)
Details
Let \(M\) be the requested maximum. The support
\[
\{0,45,49,53,94\}
\]
has the inverse displayed in `wfci127-claim-weight-85-witness`, so \(M\geq85\). The argument in `wfci127-claim-complement-upper-bound` proves \(M\leq101\). Therefore
\[
85\leq M\leq101.
\]
Both endpoints are odd, as every inverse of an odd-weight polynomial evaluates to 1 at \(x=1\). The exact maximum remains open in this fixture. Its complete normalized search space has
\[
\binom{126}{4}=10{,}009{,}125
\]
supports.
Exact cyclic multiplication verifies the supplied 127-bit inverse.
Result
Evidence: Reproduced
A replay is recorded for this computation. Inspect the replay record for its procedure and scope.
claim · Computation 2
Exact cyclic multiplication verifies the supplied 127-bit inverse.[1]
Relevance to this problem
For Densest inverse of a weight-five binary cyclic polynomial, record wfci127-claim-weight-85-witness (“A weight-five unit has inverse weight 85”) records a bound, answer, status fact, or structural consequence. The record states: Exact cyclic multiplication verifies the supplied 127-bit inverse.
Evidence
ReproducedA replay is recorded for this computation. Inspect the replay record for its procedure and scope.
Record state
established
Scope
the residue with support {0,45,49,53,94} in F_2[x]/(x^127+1)
Set
\[
f=1+x^{45}+x^{49}+x^{53}+x^{94}.
\]
In hexadecimal coefficient encoding, with the coefficient of \(x^i\) in bit \(i\),
```
f = 0x400000000022200000000001
f^{-1} = 0x3bf17593bf175d3fb175d3fb377f3fb3
```
The inverse has 85 set bits. Exact carryless cyclic multiplication gives
\[
f\,f^{-1}\equiv1\pmod{x^{127}+1}.
\]
The executable record repeats this check using integer bit operations. It also verifies the equivalent complement identity.
The complement of an inverse must have at least 26 nonzero coefficients.
Result
Evidence: Reproduced
A replay is recorded for this computation. Inspect the replay record for its procedure and scope.
claim · Computation 3
The complement of an inverse must have at least 26 nonzero coefficients.
Relevance to this problem
For Densest inverse of a weight-five binary cyclic polynomial, record wfci127-claim-complement-upper-bound (“Every inverse has weight at most 101”) records a bound, answer, status fact, or structural consequence. The record states: The complement of an inverse must have at least 26 nonzero coefficients.
Evidence
ReproducedA replay is recorded for this computation. Inspect the replay record for its procedure and scope.
Record state
established
Scope
every invertible weight-five residue in F_2[x]/(x^127+1)
Details
Write
\[
J=1+x+\cdots+x^{126}.
\]
For every weight-five \(f\), cyclic multiplication gives \(fJ=J\), because each coefficient of \(fJ\) is the parity of five. Suppose \(fg=1\), and set \(h=J+g\). Then
\[
fh=fJ+fg=J+1,
\]
whose weight is 126.
If \(t=\operatorname{wt}(h)\), the product \(fh\) is the xor of \(t\) cyclic shifts of the five-term polynomial \(f\). Hence
\[
126=\operatorname{wt}(fh)\leq5t,
\]
so \(t\geq26\). Also \(f(1)=1\) and \(fg=1\) imply \(g(1)=1\), making \(\operatorname{wt}(g)\) odd and \(t=127-\operatorname{wt}(g)\) even. It follows that
\[
\operatorname{wt}(g)=127-t\leq101.
\]
For the weight-85 witness, \(h\) has weight 42 and the verifier checks \(fh=J+1\) exactly.
Coding-based cryptography uses the same binary circulant ring and sparse factors, while the cited papers do not tabulate this length-127 extremum.
Result
Evidence: Supported
Backed by a cited source or by evidence short of a proof.
claim · Claim 1
Coding-based cryptography uses the same binary circulant ring and sparse factors, while the cited papers do not tabulate this length-127 extremum.[1][2]
Relevance to this problem
For Densest inverse of a weight-five binary cyclic polynomial, record wfci127-claim-literature-status (“The exact normalized extremum was not located in the audited literature”) records a bound, answer, status fact, or structural consequence. The record states: Coding-based cryptography uses the same binary circulant ring and sparse factors, while the cited papers do not tabulate this length-127 extremum.
Evidence
SupportedBacked by a cited source or by evidence short of a proof.
Misoczki, Tillich, Sendrier, and Barreto formulate QC-MDPC McEliece systems with binary circulant blocks and identify the circulant algebra with a quotient polynomial ring. Their work explains why sparse binary cyclic polynomials and invertibility arise together in code-based cryptography. Guo, Johansson, and Stankovski state the rank and coprimality criterion for a binary circulant block in their reaction-attack analysis.
Those sources address code construction, rank, and security. The audited passages do not give the maximum inverse weight for normalized weight-five units at length 127, nor an exhaustive table that contains it. A targeted exact computation is still needed to close the interval in this fixture.
Standard-library Python checks both product identities, both weights, and the complement upper-bound arithmetic.
Artifact
Evidence: Executable material
Executable source is recorded. Inspect its inputs and instructions before attempting a replay.
artifact · Artifact 1
Standard-library Python checks both product identities, both weights, and the complement upper-bound arithmetic.
Relevance to this problem
For Densest inverse of a weight-five binary cyclic polynomial, record wfci127-artifact-exact-witness-verifier (“Exact 127-bit cyclic-product verifier”) supplies evidence or a replay used to check the packet. The record states: Standard-library Python checks both product identities, both weights, and the complement upper-bound arithmetic.
Evidence
Executable materialExecutable source is recorded. Inspect its inputs and instructions before attempting a replay.
Record state
available
Scope
the displayed support, inverse, complement identity, and certified interval at length 127
Entry point
save code as check.py and run python3 check.py
Runtime
CPython 3, standard library only
Details
The program represents a residue by a 127-bit integer and multiplication by \(x^k\) as a cyclic rotation of its coefficient word. It verifies the displayed inverse directly. Setting \(h=J+g\), it also checks \(fh=J+1\), \(\operatorname{wt}(g)=85\), and \(\operatorname{wt}(h)=42\).
The eight-line standard output has SHA-256 digest `19774a855b737562d11bd1d30f217e6f0edee0756b2d4668c37a001a0d57161c`.
A standard-library program enumerates every support and computes inverses by binary polynomial Euclid, with a streaming result checksum.
Artifact
Evidence: Executable material
Executable source is recorded. Inspect its inputs and instructions before attempting a replay.
artifact · Artifact 2
A standard-library program enumerates every support and computes inverses by binary polynomial Euclid, with a streaming result checksum.
Relevance to this problem
For Densest inverse of a weight-five binary cyclic polynomial, record wfci127-artifact-exhaustive-search-template (“Exact exhaustive-search template”) supplies evidence or a replay used to check the packet. The record states: A standard-library program enumerates every support and computes inverses by binary polynomial Euclid, with a streaming result checksum.
Evidence
Executable materialExecutable source is recorded. Inspect its inputs and instructions before attempting a replay.
Record state
available
Scope
the algorithmic search plan for all normalized weight-five supports at length 127
Entry point
save code as exhaustive.py and run python3 exhaustive.py
Runtime
CPython 3, standard library only; the 10,009,125-support run may be lengthy
Details
The program below is a replayable exhaustive algorithm. It enumerates the 10,009,125 four-subsets of \(\{1,\ldots,126\}\). For each support it applies polynomial extended Euclid against \(x^{127}+1\), reduces a unit's Bezout coefficient cyclically, and records its inverse weight. A SHA-256 stream covers one canonical line per support, including nonunits.
This full sweep was not executed for this fixture. Its output and checksum are therefore deliberately unspecified. The completed certificate is the one-support verifier above, and the exact extremum remains between 85 and 101.
Original intake status. UNKNOWN as of 2026-07-25. An explicit unit gives 85, while a complement argument gives the universal upper bound 101. The checked sources do not settle the full acceptance condition.
The dated packet audit checked the exact title, parameter, and the terminology used by the cited primary literature.
The strongest recorded neighboring result is: An explicit unit gives 85, while a complement argument gives the universal upper bound 101.
The controlled TheoremDB corpus was checked for equivalent formulations and contains no duplicate published target.
Recorded example 1. The support {0,45,49,53,94} has inverse 0x3bf17593bf175d3fb175d3fb377f3fb3 of weight 85.
Computational notes
Exact carryless multiplication of the displayed polynomials reduces to 1 modulo x^127+1, so the current lower bound is 85. Since f(1)=1, every inverse has odd weight. Weight 127 would be the all-one polynomial, whose product with f is again all-one, giving the upper bound 125.
How the 6 records connectThe overview places each record once. The relation list includes shared dependencies and names both ends of each link.
ProblemDensest inverse of a weight-five binary cyclic polynomial
Contribute to this problemCite this problem statement
Cite the original sources separately.
Plain text
“Densest inverse of a weight-five binary cyclic polynomial.” TheoremDB. P2654. Problem statement; statement text SHA-256 0c8fceffa350b80e137d51240ca1cdad6374c4e1acf2fa9dd5d7edfb2e39833b. https://theoremdb.org/statement/?ref=P2654
BibTeX
@misc{theoremdb-problem-0c8fceffa350b80e137d51240ca1cdad6374c4e1acf2fa9dd5d7edfb2e39833b,
title = {{Densest inverse of a weight-five binary cyclic polynomial}},
howpublished = {TheoremDB},
note = {Problem statement; statement text SHA-256 0c8fceffa350b80e137d51240ca1cdad6374c4e1acf2fa9dd5d7edfb2e39833b},
url = {https://theoremdb.org/statement/?ref=P2654}
}
Once Lean accepts the draft, you can submit it while target review is pending. Your submission request is saved and continues after approval. Private checks stay private until you choose to submit.
1References
Packet source. Rafael Misoczki, Jean-Pierre Tillich, Nicolas Sendrier, and Paulo S. L. M. Barreto, MDPC-McEliece: New McEliece Variants from Moderate Density Parity-Check Codes, IACR ePrint 2012/409, sections 2 and 3; Qian Guo, Thomas Johansson, and Paul Stankovski, A Key Recovery Attack on MDPC with CCA Security Using Decoding Errors, ASIACRYPT 2016, IACR ePrint 2016/858, discussion of binary circulant rank and polynomial coprimality. Rafael Misoczki, Jean-Pierre Tillich, Nicolas Sendrier, and Paulo S. L. M. Barreto, MDPC-McEliece: New McEliece Variants from Moderate Density Parity-Check Codes, IACR ePrint 2012/409, sections 2 and 3; Qian Guo, Thomas Johansson, and Paul Stankovski, A Key Recovery Attack on MDPC with CCA Security Using Decoding Errors, ASIACRYPT 2016, IACR ePrint 2016/858, discussion of binary circulant rank and polynomial coprimality; Misoczki et al., sections 2 and 3. ↗website · reference source · web version checked 2026-07-25 · checked 2026-07-25Source use: original summary.The exact normalized extremum was not located in the audited literature. Coding-based cryptography uses the same binary circulant ring and sparse factors, while the cited papers do not tabulate this length-127 extremum.Also cited at Misoczki et al., sections 2 and 3.Also cited at wfci127-artifact-exact-witness-verifier, executed 2026-07-25.For Densest inverse of a weight-five binary cyclic polynomial: The exact normalized extremum was not located in the audited literature. Coding-based cryptography uses the same binary circulant ring and sparse factors, while the cited papers do not tabulate this length-127 extremum.Source named by the research packet.
Rafael Misoczki, Jean-Pierre Tillich, Nicolas Sendrier, and Paulo S. L. M. Barreto, MDPC-McEliece: New McEliece Variants from Moderate Density Parity-Check Codes, IACR ePrint 2012/409, sections 2 and 3; Qian Guo, Thomas Johansson, and Paul Stankovski, A Key Recovery Attack on MDPC with CCA Security Using Decoding Errors, ASIACRYPT 2016, IACR ePrint 2016/858, discussion of binary circulant rank and polynomial coprimality. Guo, Johansson, and Stankovski, binary circulant rank and coprimality discussion. ↗website · reference source · web version checked 2026-07-25 · checked 2026-07-25Source use: original summary.The exact normalized extremum was not located in the audited literature. Coding-based cryptography uses the same binary circulant ring and sparse factors, while the cited papers do not tabulate this length-127 extremum.For Densest inverse of a weight-five binary cyclic polynomial: The exact normalized extremum was not located in the audited literature. Coding-based cryptography uses the same binary circulant ring and sparse factors, while the cited papers do not tabulate this length-127 extremum.