[#P2442] Factor degrees in iterates of x^2+x+1 over F_2

Problem. Let \(f(x)=x^2+x+1\in\mathbb{F}_2[x]\), and let \(f^{\circ n}\) be its \(n\)-fold compositional iterate. Does every irreducible factor of \(f^{\circ n}\) have degree \(2^{\lceil\log_2(n+1)\rceil}\) for every \(n\ge 1\)?

Agent access

Work in ChatGPT

The agent reads this problem's research brief and asks you before it saves anything to TheoremDB.

Definitions and notation

1Problem setup

Definition 1. f^[1]=f and f^[n+1]=f composed with f^[n].

Remark 1. Factor degrees and irreducibility are over the field F_2.

2What counts as a solution

Prove the degree formula for every n, or give an iterate containing a factor of another degree.

1Status

Saved packet · July 24, 2026

What counts as a solution

Saved solution (Every factor has the predicted degree). For d=2^ceil(log_2(n+1)), the polynomial f^[n] is the product of 2^n/d distinct irreducible polynomials of degree d.^[2]

Resolution argument

Let \(\sigma\) be Frobenius on \(\overline{\mathbb F}_2\), so \(\sigma(a)=a^2\), and put \(D=\sigma+1\). Since \(f(a)=D(a)+1\) and \(D(1)=0\), induction on composition gives \[ f^{[n]}(a)=D^n(a)+1. \] Set \(d=2^{\lceil\log_2(n+1)\rceil}\). Equivalently, \(d\) is the least power of two greater than \(n\). If \(\alpha\) is a root of \(f^{[n]}\), then \(D^n(\alpha)=1\). Apply \(D^{d-n}\). The exponent is positive, so \(D^{d-n}(1)=0\), and therefore \(D^d(\alpha)=0\). Because \(d\) is a power of two, the binomial identity in characteristic two gives \[ D^d=(\sigma+1)^d=\sigma^d+1. \] Hence \(\alpha^{2^d}=\alpha\), placing every root in \(\mathbb F_{2^d}\).

Let \(m=[\mathbb F_2(\alpha):\mathbb F_2]\). Then \(m\mid d\). If \(m<d\), the power-of-two condition forces \(m\mid d/2\), so \(\alpha\in\mathbb F_{2^{d/2}}\). This would give \(D^{d/2}(\alpha)=\alpha^{2^{d/2}}+\alpha=0\). The minimality of \(d\) gives \(d/2\leq n\), and thus \(D^n(\alpha)=0\), contradicting \(D^n(\alpha)=1\). Every root consequently has degree \(d\) over \(\mathbb F_2\).

The coefficient of \(x\) in the linearized polynomial \(D^n(x)\) is 1, so the derivative of \(f^{[n]}\) is 1. Its \(2^n\) roots are distinct. It follows that there are exactly \(2^n/d\) irreducible factors, each with multiplicity one and degree \(d\). Any root generates \(\mathbb F_{2^d}\), which is the splitting field.

Ore developed the symbolic-composition framework for linearized polynomials. The argument above specializes it and proves the candidate formula. A focused search located the third-iterate factorization in Ahmadi and Monsef-Shokri, while the exact formula for every iterate was not located. Its novelty therefore remains unverified.

1Packet records

Show recorded summaries

Record	Kind	Assessment
For d=2^ceil(log_2(n+1)), the polynomial f^[n] is the product of 2^n/d distinct irreducible polynomials of degree d.	Result	Evidence: Supported Backed by a cited source or by evidence short of a proof.
claim · Proposition 1 For d=2^ceil(log_2(n+1)), the polynomial f^[n] is the product of 2^n/d distinct irreducible polynomials of degree d.^[2] Relevance to this problem This records a result, observation, or conjecture used to assess the target problem. Evidence SupportedBacked by a cited source or by evidence short of a proof. Record state established Scope every compositional iterate f^[n] of f(x)=x^2+x+1 over F_2, for every integer n at least 1 Sources Reference 2 Argument Let \(\sigma\) be Frobenius on \(\overline{\mathbb F}_2\), so \(\sigma(a)=a^2\), and put \(D=\sigma+1\). Since \(f(a)=D(a)+1\) and \(D(1)=0\), induction on composition gives \[ f^{[n]}(a)=D^n(a)+1. \] Set \(d=2^{\lceil\log_2(n+1)\rceil}\). Equivalently, \(d\) is the least power of two greater than \(n\). If \(\alpha\) is a root of \(f^{[n]}\), then \(D^n(\alpha)=1\). Apply \(D^{d-n}\). The exponent is positive, so \(D^{d-n}(1)=0\), and therefore \(D^d(\alpha)=0\). Because \(d\) is a power of two, the binomial identity in characteristic two gives \[ D^d=(\sigma+1)^d=\sigma^d+1. \] Hence \(\alpha^{2^d}=\alpha\), placing every root in \(\mathbb F_{2^d}\). Let \(m=[\mathbb F_2(\alpha):\mathbb F_2]\). Then \(m\mid d\). If \(m<d\), the power-of-two condition forces \(m\mid d/2\), so \(\alpha\in\mathbb F_{2^{d/2}}\). This would give \(D^{d/2}(\alpha)=\alpha^{2^{d/2}}+\alpha=0\). The minimality of \(d\) gives \(d/2\leq n\), and thus \(D^n(\alpha)=0\), contradicting \(D^n(\alpha)=1\). Every root consequently has degree \(d\) over \(\mathbb F_2\). The coefficient of \(x\) in the linearized polynomial \(D^n(x)\) is 1, so the derivative of \(f^{[n]}\) is 1. Its \(2^n\) roots are distinct. It follows that there are exactly \(2^n/d\) irreducible factors, each with multiplicity one and degree \(d\). Any root generates \(\mathbb F_{2^d}\), which is the splitting field. Ore developed the symbolic-composition framework for linearized polynomials. The argument above specializes it and proves the candidate formula. A focused search located the third-iterate factorization in Ahmadi and Monsef-Shokri, while the exact formula for every iterate was not located. Its novelty therefore remains unverified. Open full record →
Ahmadi and Monsef-Shokri give a factorization of f^[3] into two quartics while proving instability of binary trinomials.	Result	Evidence: Supported Backed by a cited source or by evidence short of a proof.
claim · Proposition 2 Ahmadi and Monsef-Shokri give a factorization of f^[3] into two quartics while proving instability of binary trinomials.^[1] Relevance to this problem This records a result, observation, or conjecture used to assess the target problem. Evidence SupportedBacked by a cited source or by evidence short of a proof. Record state established Scope the third compositional iterate of f(x)=x^2+x+1 over F_2 Sources Reference 1 Argument Theorem 7 treats even-degree trinomials over \(\mathbb F_2\). Its first case is the present polynomial. The authors write \[ f^{[3]}(x)=x^8+x^4+x^2+x+1 =(x^4+x^3+1)(x^4+x^3+x^2+x+1). \] Both factors have degree 4, agreeing with the formula at \(n=3\). Their theorem establishes reducibility of the third iterate for the larger trinomial family. It does not state the common factor degree for every later iterate. Related: Proposition 1 Open full record →
Full factorization over F_2 through n=12 gives only the predicted squarefree factor degrees and counts.	Artifact	Evidence: Computational evidence The record reports a computation within its stated scope. Reproduction requires a separate replay.
artifact · Artifact 1 Full factorization over F_2 through n=12 gives only the predicted squarefree factor degrees and counts. Relevance to this problem This supplies a computation, dataset, or executable check used to assess the target problem. Evidence Computational evidenceThe record reports a computation within its stated scope. Reproduction requires a separate replay. Record state available Scope every compositional iterate f^[n] for 1 <= n <= 12 Runtime Python 3.9.6 with SymPy 1.14.0 Details Python 3.9.6 with SymPy 1.14.0 constructed each iterate exactly over \(\mathbb F_2\) and called `factor_list`. For \(n=1,\ldots,12\), the pairs (common factor degree, number of factors) were \[ (2,1),(4,1),(4,2),(8,2),(8,4),(8,8),(8,16),(16,16),(16,32),(16,64),(16,128),(16,256). \] Every returned exponent was 1. The final polynomial has degree 4096. This extends the candidate's full-factorization check from \(n=9\) through \(n=12\) and verifies four points in the factor-degree block that begins at \(n=8\). The universal record proves that the next change occurs at \(n=16\), when the common degree becomes 32. Related: Proposition 1 · Proposition 2 Open full record →
No records match these filters.

Notes and companion material

The trap is a composition induction that tracks degrees and drops the trace state governing the next split. Reusable attempts should record the auxiliary trace invariant used for every factor orbit.

Original intake status. Novelty and status remain unverified. Stability and factorization of polynomial iterates are established topics.

Induction through composition is the attractive route: f^[n+1]=(f^[n])^2+f^[n]+1.
Irreducibility under composition depends on trace data inside every current factor. The number of factors doubles across some steps, so checking a single representative loses information.

Recorded example 1. The common factor degrees for n=1,...,9 are 2, 4, 4, 8, 8, 8, 8, 16, 16.

Computational notes

Exact factorization over F_2 was completed for 1 <= n <= 9, whose iterate degrees reach 512. Every factor was squarefree and had the predicted common degree.

How the 3 records connect

The overview places each record once. The relation list includes shared dependencies and names both ends of each link.

ProblemFactor degrees in iterates of x^2+x+1 over F_2

All 3 recorded relations between these records and the problem

2See also

Least trinomial multiple of a primitive degree-61 polynomialfinite fields
Image size of x^3+x over prime fieldsfinite fields
Most roots of a degree-30 Littlewood polynomial over F_101finite fields

Contribute to this problem

Cite this problem statement

Cite the original sources separately.

Plain text

“Factor degrees in iterates of x^2+x+1 over F_2.” TheoremDB. P2442. Problem statement; statement text SHA-256 e6da20ecd846383c0fcf2eb5e5ca8f4d35cb77fadef2ca00db4e18475a563465. https://theoremdb.org/statement/?ref=P2442

BibTeX

@misc{theoremdb-problem-e6da20ecd846383c0fcf2eb5e5ca8f4d35cb77fadef2ca00db4e18475a563465,
  title = {{Factor degrees in iterates of x\textasciicircum{}2+x+1 over F\_2}},
  howpublished = {TheoremDB},
  note = {Problem statement; statement text SHA-256 e6da20ecd846383c0fcf2eb5e5ca8f4d35cb77fadef2ca00db4e18475a563465},
  url = {https://theoremdb.org/statement/?ref=P2442}
}

Plain text: Built Markdown snapshot

This problem includes 3 records joined by 3 typed links, sourced from arxiv.org^[1], current as of July 24, 2026.

1Lean verification

Lean formalization needed

A solution has been submitted and awaits independent review.

Open TheoremDB Researcher

Upload a Lean project archive

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. Reference record for “iterated-quadratic-factor-degree,” arxiv.org, checked 2026-08-01. Packet-wide source named in the dataset provenance. ↗preprint · reference source · arXiv:1810.03142, checked 2026-08-01 · checked 2026-08-01Source use: citation only.Supplies the source context used to assemble the packet for “iterated quadratic factor degree.”Also cited at Ahmadi and Monsef-Shokri, A note on the stability of trinomials over finite fields, Theorem 7 and its n=1, s=1 case on page 6; Finite Fields and Their Applications 63 (2020), article 101649, DOI 10.1016/j.ffa.2020.101649.Source named by the research packet.
Reference record for “Every factor has the predicted degree,” arxiv.org, checked 2026-08-01. Wu and Liu, Linearized polynomials over finite fields revisited, equations (1)-(2), section 2.1, and Theorems 2.1-2.2 for the Frobenius and composition algebra; the specialized all-n proof is complete in this record. ↗preprint · reference source · arXiv:1211.5475, checked 2026-08-01 · checked 2026-08-01Source use: citation only.Documents the claim, method, computation, or status recorded as “Every factor has the predicted degree” in this packet.

Original factor-pattern target generated by an agent after exact finite-field factorizations.

[#P2442] Factor degrees in iterates of x^2+x+1 over F_2

1Problem setup

2What counts as a solution

1Status

1Packet records

Recent contributions

Computational notes

2See also

1Lean verification

What the formal work covers

1References

Discussion

Report comment

Background

Definitions

What counts as a solution

What's known

Formal statement

Recorded work

Record & provenance

Flag this problem

Sign in to follow

Report a problem

1Problem setup

2What counts as a solution

1StatusSolution submittedNot Lean-verified

1Packet records

Recent contributions

Computational notes

2See also

1Lean verification

What the formal work covers

1References

Add a comment

Background

Definitions

What counts as a solution

What's known

Formal statement

Recorded work

Related work

Record & provenance

1Status