Reciprocal 0,1-polynomials

DefinitionReciprocal polynomial#✓fully proved

A polynomial \(f(x) = a_0 + a_1 x + \dots + a_d x^d\) in \(\mathbb{Z}[x]\) of degree \(d\) (with \(d = 0\) for the zero polynomial) is reciprocal (palindromic) if it equals its reversal \(x^d f(1/x)\), that is, if \(a_i = a_{d-i}\) for all \(0 \le i \le d\).

def IsReciprocalPoly (f : ℤ[X]) : Prop :=
  f.reverse = f

Sources

• Pradipto Banerjee and Amit Kundu, "On an Irreducibility Question Concerning Palindromic Non-cyclotomic 0,1-Polynomials", Section 1 (terminology).

Used by 5

Used byEven–odd decomposition of a reciprocal polynomial · Even–odd decomposition of a reciprocal 0,1-polynomial · Irreducibility under repeated squaring of the variable · Characterization of reciprocal polynomials · Position of the first odd exponent

TheoremCharacterization of reciprocal polynomials#✓fully proved

A polynomial \(f \in \mathbb{Z}[x]\) of degree \(d\) (with \(d = 0\) for the zero polynomial) is reciprocal if and only if its reversal \(x^d f(1/x)\) equals \(f\).

theorem isReciprocalPoly_iff (f : ℤ[X]) :
    IsReciprocalPoly f ↔ f.reverse = f

Sources

• Pradipto Banerjee and Amit Kundu, "On an Irreducibility Question Concerning Palindromic Non-cyclotomic 0,1-Polynomials", Section 1 (terminology).

Uses 1

Statement usesReciprocal polynomial

Definition0,1-polynomial#✓fully proved

A polynomial \(f \in \mathbb{Z}[x]\) is a \(0,1\)-polynomial if every coefficient of \(f\) is \(0\) or \(1\).

def IsZeroOnePoly (f : ℤ[X]) : Prop :=
  ∀ n : ℕ, f.coeff n = 0 ∨ f.coeff n = 1

Sources

• Pradipto Banerjee and Amit Kundu, "On an Irreducibility Question Concerning Palindromic Non-cyclotomic 0,1-Polynomials", Section 1 (terminology).

Used by 6

Used byEven–odd decomposition of a reciprocal 0,1-polynomial · Irreducibility under repeated squaring of the variable · Characterization of 0,1-polynomials · Position of the first odd exponent · Square compositions of \(0,1\)-polynomials modulo \(4\) · Reducibility of \(f(x^4)\) and \(f(x^2)\) for \(0,1\)-polynomials

TheoremCharacterization of 0,1-polynomials#✓fully proved

A polynomial \(f \in \mathbb{Z}[x]\) is a \(0,1\)-polynomial if and only if, for every \(n \ge 0\), the coefficient of \(x^n\) in \(f\) is \(0\) or \(1\).

theorem isZeroOnePoly_iff (f : ℤ[X]) :
    IsZeroOnePoly f ↔ ∀ n : ℕ, f.coeff n = 0 ∨ f.coeff n = 1

Sources

• Pradipto Banerjee and Amit Kundu, "On an Irreducibility Question Concerning Palindromic Non-cyclotomic 0,1-Polynomials", Section 1 (terminology).

Uses 1

Statement uses0,1-polynomial

DefinitionNon-cyclotomic polynomial#✓fully proved

A polynomial \(f \in \mathbb{Z}[x]\) is non-cyclotomic if \(f \ne \Phi_n\) for every positive integer \(n\), where \(\Phi_n\) denotes the \(n\)-th cyclotomic polynomial.

def IsNoncyclotomic (f : ℤ[X]) : Prop :=
  ∀ n : ℕ, 0 < n → f ≠ Polynomial.cyclotomic n ℤ

Sources

• Pradipto Banerjee and Amit Kundu, "On an Irreducibility Question Concerning Palindromic Non-cyclotomic 0,1-Polynomials", Section 1 (terminology).

Used by 3

Used byIrreducibility under repeated squaring of the variable · Characterization of non-cyclotomic polynomials · Position of the first odd exponent

TheoremCharacterization of non-cyclotomic polynomials#✓fully proved

A polynomial \(f \in \mathbb{Z}[x]\) is non-cyclotomic if and only if \(f \ne \Phi_n\) for every positive integer \(n\), where \(\Phi_n\) denotes the \(n\)-th cyclotomic polynomial.

theorem isNoncyclotomic_iff (f : ℤ[X]) :
    IsNoncyclotomic f ↔
      ∀ n : ℕ, 0 < n → f ≠ Polynomial.cyclotomic n ℤ

Sources

• Pradipto Banerjee and Amit Kundu, "On an Irreducibility Question Concerning Palindromic Non-cyclotomic 0,1-Polynomials", Section 1 (terminology).

Uses 1

Statement usesNon-cyclotomic polynomial

TheoremEven–odd decomposition of a reciprocal polynomial#●ready to prove

Let \(h \in \mathbb{Z}[x]\) be an irreducible reciprocal polynomial of degree \(2k\) such that \(h \ne g(x^2)\) for every \(g \in \mathbb{Z}[x]\). Then there is exactly one \(h_e \in \mathbb{Z}[x]\) for which there is exactly one \(h_o \in \mathbb{Z}[x]\) for which there is exactly one natural number \(\ell\) such that \(h_e\) and \(h_o\) are reciprocal, \(\ell\) is odd and positive, \(\deg h_e = k\), \(\deg h_o = \max(k - \ell, 0)\), \(h(x) = h_e(x^2) + x^\ell h_o(x^2)\) and \(h_e(0)\,h_o(0) \ne 0\).

Since \(\ell\) is odd, \(h_e(x^2)\) is the even part of \(h\), and \(h_o(0) \ne 0\) then determines \(\ell\) and \(h_o\); so this amounts to a unique triple \((h_e, h_o, \ell)\).

theorem_wanted existsUnique_evenOdd_reciprocal (h : ℤ[X]) (k : ℕ)
    (hirr : Irreducible h) (hrec : IsReciprocalPoly h)
    (hdeg : h.natDegree = 2 * k)
    (hnsq : ¬ ∃ g : ℤ[X], h = g.comp (X ^ 2)) :
    ∃! he : ℤ[X], ∃! ho : ℤ[X], ∃! l : ℕ,
      IsReciprocalPoly he ∧ IsReciprocalPoly ho ∧ Odd l ∧ 0 < l ∧
        he.natDegree = k ∧ ho.natDegree = k - l ∧
        h = he.comp (X ^ 2) + X ^ l * ho.comp (X ^ 2) ∧
        he.eval 0 * ho.eval 0 ≠ 0

Sources

• Pradipto Banerjee and Amit Kundu, "On an Irreducibility Question Concerning Palindromic Non-cyclotomic 0,1-Polynomials", Lemma 2.1.

Uses 1

Statement usesReciprocal polynomial

TheoremEven–odd decomposition of a reciprocal 0,1-polynomial#●ready to prove

Let \(f \in \mathbb{Z}[x]\) be an irreducible reciprocal \(0,1\)-polynomial of degree \(2m\) such that \(f(x^2)\) is not irreducible. Then there is exactly one \(f_e \in \mathbb{Z}[x]\) for which there is exactly one \(f_o \in \mathbb{Z}[x]\) for which there is exactly one natural number \(\ell\) such that \(f_e\) and \(f_o\) are reciprocal \(0,1\)-polynomials, \(\ell\) is odd and positive, \(\deg f_e = m\), \(\deg f_o = \max(m - \ell, 0)\), \(f(x) = f_e(x^2) + x^\ell f_o(x^2)\) and \(f_e(0)\,f_o(0) \ne 0\).

Since \(\ell\) is odd, \(f_e(x^2)\) is the even part of \(f\), and \(f_o(0) \ne 0\) then determines \(\ell\) and \(f_o\); so this amounts to a unique triple \((f_e, f_o, \ell)\).

theorem_wanted existsUnique_evenOdd_zeroOne (f : ℤ[X]) (m : ℕ)
    (h01 : IsZeroOnePoly f) (hirr : Irreducible f)
    (hrec : IsReciprocalPoly f) (hdeg : f.natDegree = 2 * m)
    (hred : ¬ Irreducible (f.comp (X ^ 2))) :
    ∃! fe : ℤ[X], ∃! fo : ℤ[X], ∃! l : ℕ,
      IsZeroOnePoly fe ∧ IsZeroOnePoly fo ∧
        IsReciprocalPoly fe ∧ IsReciprocalPoly fo ∧
        Odd l ∧ 0 < l ∧
        fe.natDegree = m ∧ fo.natDegree = m - l ∧
        f = fe.comp (X ^ 2) + X ^ l * fo.comp (X ^ 2) ∧
        fe.eval 0 * fo.eval 0 ≠ 0

Sources

• Pradipto Banerjee and Amit Kundu, "On an Irreducibility Question Concerning Palindromic Non-cyclotomic 0,1-Polynomials", Lemma 2.2.

Uses 2

Statement usesReciprocal polynomial · 0,1-polynomial

TheoremPosition of the first odd exponent#●ready to prove

Let \(f \in \mathbb{Z}[x]\) be an irreducible, reciprocal, non-cyclotomic \(0,1\)-polynomial of degree \(2m\) such that \(f(x^2)\) is not irreducible. Let \(f_e, f_o \in \mathbb{Z}[x]\) and let \(\ell\) be a positive odd integer with \(f(x) = f_e(x^2) + x^\ell f_o(x^2)\), \(\deg f_e = m\) and \(\deg f_o = \max(m - \ell, 0)\), where the degree of the zero polynomial is taken to be \(0\). Then the coefficient of \(x^e\) in \(f\) is \(0\) for every \(1 \le e < \ell\), the coefficient of \(x^\ell\) in \(f\) is nonzero, and \(2\ell < m\).

theorem_wanted l_eq_min_support_and_lt (f fe fo : ℤ[X]) (m l : ℕ)
    (h01 : IsZeroOnePoly f) (hirr : Irreducible f)
    (hrec : IsReciprocalPoly f) (hnc : IsNoncyclotomic f)
    (hdeg : f.natDegree = 2 * m)
    (hdecomp : f = fe.comp (X ^ 2) + X ^ l * fo.comp (X ^ 2))
    (hfe : fe.natDegree = m) (hfo : fo.natDegree = m - l)
    (hl : Odd l) (hl0 : 0 < l)
    (hred : ¬ Irreducible (f.comp (X ^ 2))) :
    (∀ e : ℕ, 1 ≤ e → e < l → f.coeff e = 0) ∧
      f.coeff l ≠ 0 ∧ 2 * l < m

Sources

• Pradipto Banerjee and Amit Kundu, "On an Irreducibility Question Concerning Palindromic Non-cyclotomic 0,1-Polynomials", Lemma 2.3.

Uses 3

Statement usesNon-cyclotomic polynomial · Reciprocal polynomial · 0,1-polynomial

TheoremIrreducibility under repeated squaring of the variable#●ready to prove

Let \(f \in \mathbb{Z}[x]\) be an irreducible, reciprocal, non-cyclotomic \(0,1\)-polynomial with fewer than \(15\) nonzero coefficients. Then \(f(x^{2^n})\) is irreducible in \(\mathbb{Z}[x]\) for every natural number \(n\).

theorem_wanted irreducible_comp_pow_two_pow_of_card_lt (f : ℤ[X])
    (h01 : IsZeroOnePoly f) (hirr : Irreducible f)
    (hrec : IsReciprocalPoly f) (hnc : IsNoncyclotomic f)
    (hcard : f.support.card < 15) (n : ℕ) :
    Irreducible (f.comp (X ^ (2 ^ n)))

Sources

• Pradipto Banerjee and Amit Kundu, "On an Irreducibility Question Concerning Palindromic Non-cyclotomic 0,1-Polynomials", Theorem 1.1.

Uses 3

Statement usesNon-cyclotomic polynomial · Reciprocal polynomial · 0,1-polynomial

TheoremCapelli's theorem for \(f(x^r)\)#●ready to prove

Let \(f \in \mathbb{Z}[x]\) be irreducible in \(\mathbb{Z}[x]\) and let \(r \ge 2\) be an integer. Then \(f(x^r)\) is reducible if and only if either \(f(x^p)\) is reducible for some prime \(p\) dividing \(r\), or \(4\) divides \(r\) and \(f(x^4)\) is reducible. Here reducible means not irreducible in \(\mathbb{Z}[x]\).

theorem_wanted not_irreducible_comp_pow_iff (f : ℤ[X]) (r : ℕ)
    (hirr : Irreducible f) (hr : 2 ≤ r) :
    ¬ Irreducible (f.comp (X ^ r)) ↔
      (∃ p : ℕ, p.Prime ∧ p ∣ r ∧ ¬ Irreducible (f.comp (X ^ p))) ∨
        (4 ∣ r ∧ ¬ Irreducible (f.comp (X ^ 4)))

Sources

• Pradipto Banerjee and Amit Kundu, "On an Irreducibility Question Concerning Palindromic Non-cyclotomic 0,1-Polynomials", Theorem 1.2 (Capelli; the root-theoretic equivalents stated there are omitted).

TheoremSquare compositions of \(0,1\)-polynomials modulo \(4\)#●ready to prove

Let \(f \in \mathbb{Z}[x]\) be irreducible in \(\mathbb{Z}[x]\), with every coefficient equal to \(0\) or \(1\) and with constant term \(f(0) = 1\). If \(f(x^2)\) is not irreducible in \(\mathbb{Z}[x]\), then \(f(x^2) \equiv f(x)\,f(-x) \pmod 4\) as polynomials, that is, the two polynomials have the same image in \((\mathbb{Z}/4\mathbb{Z})[x]\).

theorem_wanted map_comp_sq_eq_mul (f : ℤ[X])
    (h01 : IsZeroOnePoly f) (hirr : Irreducible f) (hf0 : f.coeff 0 = 1)
    (hred : ¬ Irreducible (f.comp (X ^ 2))) :
    (f.comp (X ^ 2)).map (Int.castRingHom (ZMod 4)) =
      (f * f.comp (-X)).map (Int.castRingHom (ZMod 4))

Sources

• Pradipto Banerjee and Amit Kundu, "On an Irreducibility Question Concerning Palindromic Non-cyclotomic 0,1-Polynomials", Theorem 1.3.

Uses 1

Statement uses0,1-polynomial

TheoremReducibility of \(f(x^4)\) and \(f(x^2)\) for \(0,1\)-polynomials#●ready to prove

Let \(f \in \mathbb{Z}[x]\) be irreducible in \(\mathbb{Z}[x]\) and of positive degree, with every coefficient equal to \(0\) or \(1\) and with constant term \(f(0) = 1\). Then \(f(x^4)\) is not irreducible in \(\mathbb{Z}[x]\) if and only if \(f(x^2)\) is not irreducible in \(\mathbb{Z}[x]\).

theorem_wanted not_irreducible_comp_four_iff (f : ℤ[X])
    (h01 : IsZeroOnePoly f) (hirr : Irreducible f) (hf0 : f.coeff 0 = 1)
    (hdeg : 0 < f.natDegree) :
    ¬ Irreducible (f.comp (X ^ 4)) ↔ ¬ Irreducible (f.comp (X ^ 2))

Sources

• Pradipto Banerjee and Amit Kundu, "On an Irreducibility Question Concerning Palindromic Non-cyclotomic 0,1-Polynomials", Theorem 1.4.

Uses 1

Statement uses0,1-polynomial

6 fully proved7 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.