Algebrization barrier

DefinitionMultilinear extension of a Boolean function#✓fully proved

Identify the booleans true and false with \(1\) and \(0\). Let \(F\) be a field, \(n\) a natural number and \(f : \{0,1\}^n \to \{0,1\}\). The multilinear extension of \(f\) at a point \(x = (x_0, \dots, x_{n-1}) \in F^n\) is

\[\sum_{a \in \{0,1\}^n} f(a) \prod_{i=0}^{n-1} \ell_{a_i}(x_i),\]

where \(f(a) \in \{0, 1\}\) is read in \(F\), \(\ell_1(t) = t\) and \(\ell_0(t) = 1 - t\).

noncomputable def multilinearExt {n : ℕ} {F : Type*} [Field F]
    (f : (Fin n → Bool) → Bool) (x : Fin n → F) : F :=
  ∑ a : Fin n → Bool, (if f a then 1 else 0) *
    ∏ i : Fin n, (if a i then x i else 1 - x i)

Used by 1

Used byAnswer bits of the algebraic extension oracle

DefinitionRestriction of an oracle to inputs of length \(n\)#✓fully proved

For a function \(B\) from bitstrings to booleans and a natural number \(n\), the restriction of \(B\) to inputs of length \(n\) is the function on \(\{0,1\}^n\) sending \(a = (a_0, \dots, a_{n-1})\) to \(B(a_0 a_1 \cdots a_{n-1})\), the value of \(B\) at the bitstring \(a\).

def baseAt (B : List Bool → Bool) (n : ℕ) : (Fin n → Bool) → Bool :=
  fun a => B (List.ofFn a)

Used by 1

Used byAnswer bits of the algebraic extension oracle

DefinitionCoefficient bitstring of a polynomial over \(\mathbb{F}_2\)#✓fully proved

For a polynomial \(q\) over \(\mathbb{F}_2 = \mathbb{Z}/2\mathbb{Z}\) and a natural number \(n\), the coefficient bitstring of \(q\) with parameter \(n\) is the bitstring \(b_0 b_1 \cdots b_{n+1}\) of length \(n + 2\) in which \(b_i\) is true exactly when the coefficient of \(X^i\) in \(q\) equals \(1\).

def polyBits (q : Polynomial (ZMod 2)) (n : ℕ) : List Bool :=
  (List.range (n + 2)).map (fun i => decide (q.coeff i = 1))

Used by 1

Used byAlgebraic extension oracles

DefinitionAnswer bits of the algebraic extension oracle#✓fully proved

Let \(n\) be a natural number, let \(p\) be a monic irreducible polynomial of degree \(n + 1\) over \(\mathbb{F}_2 = \mathbb{Z}/2\mathbb{Z}\), let \(F = \mathbb{F}_2[X]/(p)\) with \(\alpha\) the class of \(X\), let \(B\) be a function from bitstrings to booleans, and let \(\tilde B_n\) be the multilinear extension over \(F\) of the restriction of \(B\) to inputs of length \(n\). Given a list \((e_0, e_1, \ldots)\) of bitstrings and an index \(j\) with \(0 \le j \le n\), let \(e_{i,k} \in \{0, 1\}\) be the bit of \(e_i\) at position \(k\), counting from \(0\), where a missing list entry or a missing bit counts as \(0\), and let \(x \in F^n\) be the point with coordinates \(x_i = \sum_{k=0}^{n} e_{i,k} \alpha^k\) for \(i < n\). The answer bit is true exactly when the coefficient of \(\alpha^j\) in \(\tilde B_n(x)\), written in the basis \(1, \alpha, \dots, \alpha^n\) of \(F\) over \(\mathbb{F}_2\), equals \(1\).

The index \(j\) ranges over \(0, \dots, n\) only: an out-of-range index must be rejected by the caller, not reduced modulo \(n + 1\).

noncomputable def extAnswer {p : Polynomial (ZMod 2)} [Fact (Irreducible p)] (hp : p.Monic)
    (n : ℕ) (_hdeg : p.natDegree = n + 1) (B : List Bool → Bool)
    (pt : List (List Bool)) (j : Fin p.natDegree) : Bool :=
  decide (((AdjoinRoot.powerBasisAux' hp).repr
    (multilinearExt (baseAt B n)
      (fun i => AdjoinRoot.mk p (∑ k : Fin p.natDegree,
        Polynomial.monomial k.val
          (if (pt.getD i.val []).getD k.val false then (1 : ZMod 2) else 0))))
    j = 1))

Uses 2 · Used by 1

Statement usesRestriction of an oracle to inputs of length \(n\) · Multilinear extension of a Boolean function

Used byAlgebraic extension oracles

DefinitionAlgebraic extension oracles#✓fully proved

Let \(B\) and \(O\) be oracles, that is, functions from bitstrings to booleans. Then \(O\) is an algebraic extension of \(B\) when there are polynomials \(\pi_0, \pi_1, \pi_2, \ldots\) over \(\mathbb{F}_2 = \mathbb{Z}/2\mathbb{Z}\), each \(\pi_n\) monic and irreducible of degree \(n + 1\), with the following two properties, where \(F_n\) is the field \(\mathbb{F}_2[X]/(\pi_n)\), \(\alpha_n\) is the class of \(X\) in \(F_n\), and \(\tilde B_n\) is the multilinear extension over \(F_n\) of the restriction of \(B\) to inputs of length \(n\). First, the map sending a bitstring \(u\) to the coefficient bitstring of \(\pi_{|u|}\) with parameter \(|u|\) (whose bits say which of the coefficients of \(X^0, \dots, X^{|u|+1}\) equal \(1\)) is polynomial-time computable. Second, let \(y\) be a bitstring. If \(y\) decodes, under the canonical bitstring encoding of triples, to a triple \((u, (e_0, \dots, e_{m-1}), j)\) of a bitstring \(u\), a list of bitstrings and a natural number \(j\) such that, writing \(n = |u|\), we have \(m = n\), every \(e_i\) has length \(n + 1\) and \(j \le n\), then \(O(y)\) is true exactly when the coefficient of \(\alpha_n^j\) in \(\tilde B_n(x)\), written in the basis \(1, \alpha_n, \dots, \alpha_n^n\) of \(F_n\) over \(\mathbb{F}_2\), equals \(1\). Here \(x \in F_n^n\) is the point with coordinates \(x_i = \sum_{k=0}^{n} e_{i,k} \alpha_n^k\), where \(e_{i,k} \in \{0, 1\}\) is the bit of \(e_i\) at position \(k\), counting from \(0\). Otherwise, in particular when \(y\) does not decode, \(O(y)\) is false.

Every malformed query is answered false, so an oracle machine cannot route around the algebraic structure through invalid encodings, and an out-of-range \(j\) does not wrap around to coordinate \(0\).

MetaMathlibExt.Complexity.KeyTheorems.Algebrization.IsAlgebraicExtension · 15 lines

def IsAlgebraicExtension (B O : List Bool → Bool) : Prop :=
  ∃ (irr : ℕ → Polynomial (ZMod 2))
    (hspec : ∀ n, (irr n).Monic ∧ (irr n).natDegree = n + 1 ∧ Irreducible (irr n)),
    IsPolyTime (fun u : List Bool => polyBits (irr u.length) u.length) ∧
    ∀ y : List Bool, O y =
      match MetaMathlibExt.BitstringEncoding.bitDecode
          (α := List Bool × List (List Bool) × ℕ) y with
      | some (u, pt, j) =>
        if h : pt.length = u.length ∧ (∀ e ∈ pt, e.length = u.length + 1) ∧
            j < u.length + 1 then
          @extAnswer (irr u.length) ⟨(hspec u.length).2.2⟩ (hspec u.length).1
            u.length (hspec u.length).2.1 B pt
            ⟨j, by rw [(hspec u.length).2.1]; exact h.2.2⟩
        else false
      | none => false

Uses 11 · Used by 1

Statement usesBitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks · Answer bits of the algebraic extension oracle · Coefficient bitstring of a polynomial over \(\mathbb{F}_2\) · Polynomial-time computable functions

Used byAaronson-Wigderson: the algebrization barrier

TheoremAaronson-Wigderson: the algebrization barrier#●ready to prove

Call an oracle a function from bitstrings to booleans. There are oracles \(B\) and \(\tilde B\) such that \(\tilde B\) is an algebraic extension of \(B\) and \(\mathsf{P}^B = \mathsf{NP}^{\tilde B}\). There are also oracles \(B\) and \(\tilde B\) such that \(\tilde B\) is an algebraic extension of \(B\) and \(\mathsf{NP}^B\) is not contained in \(\mathsf{P}^{\tilde B}\).

public theorem_wanted aaronson_wigderson_algebrization :
    (∃ B Bext : List Bool → Bool, IsAlgebraicExtension B Bext ∧
      PWithOracle B = NPWithOracle Bext) ∧
    (∃ B Bext : List Bool → Bool, IsAlgebraicExtension B Bext ∧
      ¬ (NPWithOracle B ⊆ PWithOracle Bext))

Sources

• S. Aaronson and A. Wigderson, "Algebrization: A new barrier in complexity theory", Proceedings of the Fortieth Annual ACM Symposium on Theory of Computing (STOC 2008), 731-740 (journal version in ACM Transactions on Computation Theory 1 (2009)).

Uses 5

Statement usesNP relative to an oracle · Polynomial time with an oracle · Algebraic extension oracles · Complexity classes · Decision problems

5 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.