Quadratic equation satisfiability

This file defines the QESAT language and the exponential-length PCP for it.

@[reducible, inline]

abbrev QESAT (F : Type) [Field F] (n : ℕ) : Set (List (CPoly.CMvPolynomial n F))

Equations

• QESAT F n polys = ((∀ p ∈ polys, p.totalDegree ≤ 2) ∧ ∃ (a : Fin n → F), ∀ p ∈ polys, CPoly.CMvPolynomial.eval a p = 0)

def QESAT.size (F : Type) [Field F] [Fintype F] (n : ℕ) (polys : List (CPoly.CMvPolynomial n F)) : ℕ

The size of a QESAT instance if it was a binary string TODO: the proper way would be to use this: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Computability/Encoding.html

Equations

• QESAT.size F n polys = polys.length * (n + 1) ^ 2

theorem QESAT_exp_PCP {vars : ℕ} : ∃ (q : ℕ) (r : Polynomial ℕ), QESAT (ZMod 2) vars ∈ PCP (QESAT.size (ZMod 2) vars) 0 (1 / 2) (ZMod 2) (fun (n : ℕ) => 2 ^ n) (fun (x : ℕ) => q) fun (x : ℕ) => Polynomial.eval x r