Documentation

def Cslib.Complexity.IsCanonicalMonomial (m : List ℕ) :

Prop

A canonical multilinear monomial is a strictly increasing list of variable indices.

Instances For

theorem Cslib.Complexity.IsCanonicalMonomial.nodup {m : List ℕ} (hm : IsCanonicalMonomial m) :

m.Nodup

theorem Cslib.Complexity.IsCanonicalMonomial.eq_of_toFinset_eq {m₁ m₂ : List ℕ} (hm₁ : IsCanonicalMonomial m₁) (hm₂ : IsCanonicalMonomial m₂) (h : m₁.toFinset = m₂.toFinset) :

m₁ = m₂

def Cslib.Complexity.IsCanonicalEquation (eq : List (List ℕ)) :

Prop

A sparse 𝔽₂ polynomial equation is canonical when its monomial list is duplicate-free and every monomial is strictly increasing.

Instances For

theorem Cslib.Complexity.isCanonicalEquation_nil :

IsCanonicalEquation []

def Cslib.Complexity.evalMonomialList (eq : List (List ℕ)) (σ : ℕ → Bool) :

Bool

Evaluate a sparse 𝔽₂ monomial list on a Boolean assignment σ : ℕ → Bool.

Instances For

def Cslib.Complexity.evalSystem (sys : List (List (List ℕ))) (σ : ℕ → Bool) :

Bool

Evaluate a sparse 𝔽₂ polynomial system (true iff every equation evaluates to false).

Instances For

@[simp]

theorem Cslib.Complexity.evalMonomialList_nil (σ : ℕ → Bool) :

evalMonomialList [] σ = false

@[simp]

theorem Cslib.Complexity.evalMonomialList_cons (m : List ℕ) (eq : List (List ℕ)) (σ : ℕ → Bool) :

evalMonomialList (m :: eq) σ = (m.all σ ^^ evalMonomialList eq σ)

theorem Cslib.Complexity.evalMonomialList_singleton (m : List ℕ) (σ : ℕ → Bool) :

evalMonomialList [m] σ = m.all σ

theorem Cslib.Complexity.evalMonomialList_append (eq1 eq2 : List (List ℕ)) (σ : ℕ → Bool) :

evalMonomialList (eq1 ++ eq2) σ = (evalMonomialList eq1 σ ^^ evalMonomialList eq2 σ)

theorem Cslib.Complexity.evalSystem_eq_true_iff (sys : List (List (List ℕ))) (σ : ℕ → Bool) :

evalSystem sys σ = true ↔ ∀ eq ∈ sys, evalMonomialList eq σ = false

theorem Cslib.Complexity.bitVal_evalMonomialList_eq_sum_monomial {eq : List (List ℕ)} (heq : IsCanonicalEquation eq) (σ : ℕ → Bool) :

BitString.bitVal (ZMod 2) (evalMonomialList eq σ) = ∑ S ∈ (List.map List.toFinset eq).toFinset, BitString.monomial (ZMod 2) S σ

On a canonical equation eq, reading evalMonomialList eq σ in ZMod 2 equals the Finset sum of BitString.monomial (ZMod 2) over (eq.map List.toFinset).toFinset.

theorem Cslib.Complexity.bitVal_evalMonomialList_mem_lowDegree {k : ℕ} {eq : List (List ℕ)} (hdeg : ∀ m ∈ eq, m.length ≤ k) :

(fun (σ : ℕ → Bool) => BitString.bitVal (ZMod 2) (evalMonomialList eq σ)) ∈ BitString.lowDegree (ZMod 2) ℕ k

Every sparse 𝔽₂ equation whose monomials have length at most k defines a Boolean-cube function of ZMod 2-degree at most k.

def Cslib.Complexity.toggleMonomial (eq : List (List ℕ)) (m : List ℕ) :

Toggle the presence of monomial m in a duplicate-free list eq modulo 2.

Instances For

def Cslib.Complexity.reduceEquation (eq : List (List ℕ)) :

Cancel duplicate monomials in eq modulo 2 by folding toggleMonomial from [].

Instances For

def Cslib.Complexity.xorEquation (eq1 eq2 : List (List ℕ)) :

Executable mod-2 symmetric difference of two sparse 𝔽₂ equations.

Instances For

theorem Cslib.Complexity.nodup_reduceEquation (eq : List (List ℕ)) :

(reduceEquation eq).Nodup

theorem Cslib.Complexity.mem_of_mem_reduceEquation {eq : List (List ℕ)} {m : List ℕ} (hm : m ∈ reduceEquation eq) :

m ∈ eq

theorem Cslib.Complexity.length_reduceEquation_le (eq : List (List ℕ)) :

(reduceEquation eq).length ≤ eq.length

theorem Cslib.Complexity.evalMonomialList_reduceEquation (eq : List (List ℕ)) (σ : ℕ → Bool) :

evalMonomialList (reduceEquation eq) σ = evalMonomialList eq σ

theorem Cslib.Complexity.nodup_xorEquation (eq1 eq2 : List (List ℕ)) :

(xorEquation eq1 eq2).Nodup

theorem Cslib.Complexity.mem_of_mem_xorEquation {eq1 eq2 : List (List ℕ)} {m : List ℕ} (hm : m ∈ xorEquation eq1 eq2) :

m ∈ eq1 ∨ m ∈ eq2

theorem Cslib.Complexity.isCanonicalEquation_xorEquation {eq1 eq2 : List (List ℕ)} (h1 : IsCanonicalEquation eq1) (h2 : IsCanonicalEquation eq2) :

IsCanonicalEquation (xorEquation eq1 eq2)

xorEquation preserves canonical sorted monomials and Nodup.

theorem Cslib.Complexity.evalMonomialList_xorEquation (eq1 eq2 : List (List ℕ)) (σ : ℕ → Bool) :

evalMonomialList (xorEquation eq1 eq2) σ = (evalMonomialList eq1 σ ^^ evalMonomialList eq2 σ)

xorEquation evaluates to the Boolean XOR of the two equations' evaluations.

theorem Cslib.Complexity.length_xorEquation_le (eq1 eq2 : List (List ℕ)) :

(xorEquation eq1 eq2).length ≤ eq1.length + eq2.length

xorEquation outputs at most eq1.length + eq2.length monomials.

2. Executable Clause Falsification & Parity-Row Compiler (§6 eq. (6.1) & §6.3) #

def Cslib.Complexity.insertSorted (m : List ℕ) (v : ℕ) :

Insert v into a strictly increasing monomial m, omitting duplicates.

Instances For

def Cslib.Complexity.sortDedup (vs : List ℕ) :

Canonical strictly increasing deduplication of variable indices.

Instances For

theorem Cslib.Complexity.mem_insertSorted {m : List ℕ} {v u : ℕ} :

u ∈ insertSorted m v ↔ u ∈ m ∨ u = v

@[simp]

theorem Cslib.Complexity.toFinset_insertSorted (m : List ℕ) (v : ℕ) :

(insertSorted m v).toFinset = insert v m.toFinset

theorem Cslib.Complexity.isCanonicalMonomial_insertSorted {m : List ℕ} (hm : IsCanonicalMonomial m) (v : ℕ) :

IsCanonicalMonomial (insertSorted m v)

theorem Cslib.Complexity.all_insertSorted (m : List ℕ) (v : ℕ) (σ : ℕ → Bool) :

(insertSorted m v).all σ = (m.all σ && σ v)

theorem Cslib.Complexity.isCanonicalMonomial_sortDedup (vs : List ℕ) :

IsCanonicalMonomial (sortDedup vs)

theorem Cslib.Complexity.nodup_sortDedup (vs : List ℕ) :

(sortDedup vs).Nodup

@[simp]

theorem Cslib.Complexity.mem_sortDedup {vs : List ℕ} {u : ℕ} :

u ∈ sortDedup vs ↔ u ∈ vs

@[simp]

theorem Cslib.Complexity.toFinset_sortDedup (vs : List ℕ) :

(sortDedup vs).toFinset = vs.toFinset

def Cslib.Complexity.isTautologicalClause (c : Logic.PL.Clause ℕ) :

Bool

Check whether clause c contains both (v, true) and (v, false) for some v.

Instances For

def Cslib.Complexity.posVars (c : Logic.PL.Clause ℕ) :

Sorted distinct positive-literal variables of c.

Instances For

def Cslib.Complexity.negVars (c : Logic.PL.Clause ℕ) :

Sorted distinct negative-literal variables of c.

Instances For

def Cslib.Complexity.expandPosVars (base vs : List ℕ) :

Expand ∏_{v ∈ vs} (1 ⊕ x_v) starting from a canonical base monomial base.

Instances For

def Cslib.Complexity.compileClause (c : Logic.PL.Clause ℕ) :

Compile the falsification indicator v_c(x) = !c.eval x of a clause c : Clause ℕ into a canonical sparse 𝔽₂ polynomial (§6, p. 39). Tautological clauses compile to [] (0).

Instances For

theorem Cslib.Complexity.isCanonicalEquation_compileClause (c : Logic.PL.Clause ℕ) :

IsCanonicalEquation (compileClause c)

compileClause c always produces a canonical sparse 𝔽₂ equation.

theorem Cslib.Complexity.mem_clause_of_mem_compileClause {c : Logic.PL.Clause ℕ} {m : List ℕ} {v : ℕ} (hm : m ∈ compileClause c) (hv : v ∈ m) :

∃ (b : Bool), (v, b) ∈ c

Every variable occurring in compileClause c is a variable of c.

theorem Cslib.Complexity.length_mem_compileClause_le {c : Logic.PL.Clause ℕ} {m : List ℕ} (hm : m ∈ compileClause c) :

m.length ≤ List.length c

Every monomial in compileClause c has length at most c.length.

theorem Cslib.Complexity.length_compileClause_le (c : Logic.PL.Clause ℕ) :

(compileClause c).length ≤ 2 ^ List.length c

compileClause c expands into at most 2 ^ c.length monomials.

theorem Cslib.Complexity.evalMonomialList_compileClause (c : Logic.PL.Clause ℕ) (σ : ℕ → Bool) :

evalMonomialList (compileClause c) σ = !Logic.PL.Clause.eval σ c

Exact clause falsification semantics (§6, p. 39): compileClause c evaluates to !c.eval σ for every assignment σ.

def Cslib.Complexity.compileParityRow (φ : Logic.PL.CNF ℕ) (row : List Bool) :

Compile a parity-check row row : List Bool on φ : CNF ℕ into a sparse 𝔽₂ polynomial equation by XORing compileClause φ[e] over e < φ.length with row.getD e false = true.

Instances For

def Cslib.Complexity.compileParitySystem (φ : Logic.PL.CNF ℕ) (rows : List (List Bool)) :

List (List (List ℕ))

Compile a list of parity-check rows on φ : CNF ℕ into a sparse 𝔽₂ polynomial system.

Instances For

theorem Cslib.Complexity.isCanonicalEquation_compileParityRow (φ : Logic.PL.CNF ℕ) (row : List Bool) :

IsCanonicalEquation (compileParityRow φ row)

theorem Cslib.Complexity.length_mem_compileParityRow_le {k : ℕ} {φ : Logic.PL.CNF ℕ} (hφ : ∀ c ∈ φ, List.length c ≤ k) (row : List Bool) {m : List ℕ} (hm : m ∈ compileParityRow φ row) :

m.length ≤ k

When every clause of φ has width at most k, every monomial in compileParityRow φ row has degree at most k.

theorem Cslib.Complexity.mem_vars_of_mem_compileParityRow {φ : Logic.PL.CNF ℕ} {row : List Bool} {m : List ℕ} {v : ℕ} (hm : m ∈ compileParityRow φ row) (hv : v ∈ m) :

v ∈ φ.vars

theorem Cslib.Complexity.length_compileParityRow_le {k : ℕ} {φ : Logic.PL.CNF ℕ} (hφ : ∀ c ∈ φ, List.length c ≤ k) (row : List Bool) :

(compileParityRow φ row).length ≤ List.count true row * 2 ^ k

Row sparsity bound (§6.2, p. 42): when every clause of φ has width at most k, compileParityRow φ row contains at most row.count true * 2 ^ k monomials.

theorem Cslib.Complexity.evalMonomialList_compileParityRow_eq_dotProduct (φ : Logic.PL.CNF ℕ) (row : List Bool) (σ : ℕ → Bool) :

evalMonomialList (compileParityRow φ row) σ = (fun (e : Fin (List.length φ)) => row.getD (↑e) false) ⬝ᵥ φ.violations σ

Exact parity-row semantics (§6 eq. (6.1)): compileParityRow φ row evaluates to the 𝔽₂ dot product of row with φ.violations σ.

theorem Cslib.Complexity.evalSystem_compileParitySystem_iff_passesTests (φ : Logic.PL.CNF ℕ) (rows : List (List Bool)) (σ : ℕ → Bool) :

evalSystem (compileParitySystem φ rows) σ = true ↔ BitString.PassesTests φ.violations (List.map (fun (row : List Bool) (e : Fin (List.length φ)) => row.getD (↑e) false) rows) σ

System acceptance equivalence: σ is a common zero of compileParitySystem φ rows over 𝔽₂ if and only if σ passes all parity tests represented by rows on φ.violations.

def Cslib.Complexity.compileClauseBounded (k : ℕ) (c : Logic.PL.Clause ℕ) :

Width-k guarded clause compiler (agrees with compileClause on clauses of width ≤ k).

Instances For

def Cslib.Complexity.compileParityRowBounded (k : ℕ) (φ : Logic.PL.CNF ℕ) (row : List Bool) :

Width-k guarded parity-row compiler.

Instances For

def Cslib.Complexity.compileParitySystemBounded (k : ℕ) (φ : Logic.PL.CNF ℕ) (rows : List (List Bool)) :

List (List (List ℕ))

Width-k guarded parity-system compiler.

Instances For

theorem Cslib.Complexity.compileParitySystemBounded_eq_compileParitySystem {k : ℕ} {φ : Logic.PL.CNF ℕ} (hφ : ∀ c ∈ φ, List.length c ≤ k) (rows : List (List Bool)) :

compileParitySystemBounded k φ rows = compileParitySystem φ rows

3. Executable Heavy-Variable Finder & Variable Restriction (§5.5, pp. 38–39) #

def Cslib.Complexity.equationVars (eq : List (List ℕ)) :

Canonical duplicate-free variable scope of an equation eq.

Instances For

def Cslib.Complexity.varDegree (v : ℕ) (sys : List (List (List ℕ))) :

ℕ

Incidence degree of variable v in sys: number of equation scopes containing v.

Instances For

def Cslib.Complexity.findHeavyVar (n b₀ : ℕ) (sys : List (List (List ℕ))) :

Option ℕ

First variable v < n with varDegree v sys > b₀, or none if none exists (§5.5, p. 38).

Instances For

def Cslib.Complexity.restrictEquation (v : ℕ) (val : Bool) (eq : List (List ℕ)) :

Substitute x_v = val into eq over 𝔽₂, dropping monomials containing v when val = false and erasing v then cancelling mod-2 duplicates when val = true (§5.5, p. 38).

Instances For

def Cslib.Complexity.restrictSystem (v : ℕ) (val : Bool) (sys : List (List (List ℕ))) :

List (List (List ℕ))

Substitute x_v = val across every equation of a sparse 𝔽₂ system.

Instances For

@[simp]

theorem Cslib.Complexity.mem_equationVars {eq : List (List ℕ)} {v : ℕ} :

v ∈ equationVars eq ↔ ∃ m ∈ eq, v ∈ m

theorem Cslib.Complexity.findHeavyVar_eq_some_iff {n b₀ : ℕ} {sys : List (List (List ℕ))} {v : ℕ} :

findHeavyVar n b₀ sys = some v ↔ v < n ∧ b₀ < varDegree v sys ∧ ∀ u < v, varDegree u sys ≤ b₀

findHeavyVar n b₀ sys = some v iff v < n is minimal with varDegree v sys > b₀.

theorem Cslib.Complexity.findHeavyVar_eq_none_iff {n b₀ : ℕ} {sys : List (List (List ℕ))} :

findHeavyVar n b₀ sys = none ↔ ∀ v < n, varDegree v sys ≤ b₀

findHeavyVar n b₀ sys = none iff every v < n occurs in at most b₀ equation scopes.

theorem Cslib.Complexity.exists_sublist_of_mem_restrictEquation {v : ℕ} {val : Bool} {eq : List (List ℕ)} {m' : List ℕ} (hm' : m' ∈ restrictEquation v val eq) :

∃ m ∈ eq, m'.Sublist m

theorem Cslib.Complexity.length_mem_restrictEquation_le {k v : ℕ} {val : Bool} {eq : List (List ℕ)} (hdeg : ∀ m ∈ eq, m.length ≤ k) {m' : List ℕ} (hm' : m' ∈ restrictEquation v val eq) :

m'.length ≤ k

restrictEquation preserves any monomial degree bound ≤ k.

theorem Cslib.Complexity.length_restrictEquation_le (v : ℕ) (val : Bool) (eq : List (List ℕ)) :

(restrictEquation v val eq).length ≤ eq.length

restrictEquation never increases the number of monomials.

theorem Cslib.Complexity.not_mem_of_mem_restrictEquation {v : ℕ} {val : Bool} {eq : List (List ℕ)} {m' : List ℕ} (hm' : m' ∈ restrictEquation v val eq) :

v ∉ m'

restrictEquation v val eq eliminates v from all output monomials.

theorem Cslib.Complexity.evalMonomialList_restrictEquation (v : ℕ) (val : Bool) (eq : List (List ℕ)) (σ : ℕ → Bool) :

evalMonomialList (restrictEquation v val eq) σ = evalMonomialList eq (Function.update σ v val)

Exact variable-restriction semantics (§5.5, p. 38): evaluating restrictEquation v val eq on σ agrees with evaluating eq on Function.update σ v val.

4. Polynomial-Time Complexity Proofs (Plain `ComputableInPolyTime`) #

Turing.MultiTapeTM.ComputableInPolyTime reduceEquation (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat))

theorem Cslib.Complexity.computableInPolyTime_reduceEquation :

Mod-2 duplicate monomial cancellation reduceEquation is polynomial-time.

Mod-2 equation symmetric difference xorEquation is polynomial-time.

Turing.MultiTapeTM.ComputableInPolyTime (compileClauseBounded k) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encBool)) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat))

theorem Cslib.Complexity.computableInPolyTime_compileClauseBounded (k : ℕ) :

For any fixed width bound k : ℕ, compiling a clause with width guard k into a canonical sparse 𝔽₂ polynomial is polynomial-time.

theorem Cslib.Complexity.length_enc_reduceEquation_le (l : List (List ℕ)) :

((Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)) (reduceEquation l)).length ≤ ((Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)) l).length

Reducing an equation modulo 2 (reduceEquation) does not increase its encoded length.

theorem Cslib.Complexity.computableInPolyTime_compileParityRowBounded (k : ℕ) {encRow : List Bool ↪ List Bool} [Turing.MultiTapeTM.ListEncoding Turing.MultiTapeTM.encBool encRow] [Turing.MultiTapeTM.SizedListEncoding Turing.MultiTapeTM.encBool encRow] :

Turing.MultiTapeTM.ComputableInPolyTime (fun (p : Logic.PL.CNF ℕ × List Bool) => compileParityRowBounded k p.1 p.2) (Turing.MultiTapeTM.encPair encCNF encRow) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat))

For any fixed width bound k : ℕ, compiling a parity-check row on φ : CNF ℕ is polynomial-time (for any sized Boolean list encoding encRow, such as encBits or encList encBool).

For any fixed width bound k : ℕ, compiling a list of parity-check rows on φ : CNF ℕ into a sparse degree-≤ k 𝔽₂ polynomial system is polynomial-time.

theorem Cslib.Complexity.computableInPolyTime_varDegree :

Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × List (List (List ℕ))) => varDegree p.1 p.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)))) Turing.MultiTapeTM.encUnary

Computing varDegree v sys (returned in unary) is polynomial-time.

Finding the first heavy variable v < n with varDegree v sys > b₀ (n in unary, b₀ in binary, result in encOption encNat) is polynomial-time.

theorem Cslib.Complexity.computableInPolyTime_findHeavyVar_apply {α : Type} {encIn : α ↪ List Bool} {fn fb : α → ℕ} {fsys : α → List (List (List ℕ))} (hn : Turing.MultiTapeTM.ComputableInPolyTime fn encIn Turing.MultiTapeTM.encUnary) (hb : Turing.MultiTapeTM.ComputableInPolyTime fb encIn Turing.MultiTapeTM.encNat) (hsys : Turing.MultiTapeTM.ComputableInPolyTime fsys encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)))) :

Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => findHeavyVar (fn x) (fb x) (fsys x)) encIn (Turing.MultiTapeTM.encOption Turing.MultiTapeTM.encNat)

Substituting x_v = val into a sparse 𝔽₂ equation (restrictEquation) is polynomial-time.

theorem Cslib.Complexity.computableInPolyTime_restrictEquation_apply {α : Type} {encIn : α ↪ List Bool} {fv : α → ℕ} {fval : α → Bool} {feq : α → List (List ℕ)} (hv : Turing.MultiTapeTM.ComputableInPolyTime fv encIn Turing.MultiTapeTM.encNat) (hval : Turing.MultiTapeTM.ComputableInPolyTime fval encIn Turing.MultiTapeTM.encBool) (heq : Turing.MultiTapeTM.ComputableInPolyTime feq encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat))) :

Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => restrictEquation (fv x) (fval x) (feq x)) encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat))

Substituting x_v = val across a sparse 𝔽₂ system (restrictSystem) is polynomial-time.