Bounded-degree circuit consistency polynomials

In characteristic two, 1 + w + rhs is the indicator of Boolean gate consistency. Input-copy routing bounds the uses of external variables as well as gate variables. The output literal is included explicitly.

noncomputable def MIPRE.SAT.Circuit.gateArith {F : Type u_1} [Field F] (C : Circuit) (k : ℕ) : Gate → MvPolynomial (ℕ ⊕ ℕ) F

A gate's right-hand-side polynomial, with routed input copies.

Equations

• C.gateArith k (MIPRE.SAT.Gate.input i) = MvPolynomial.X (C.inputRef k i)
• C.gateArith k (MIPRE.SAT.Gate.const b) = MvPolynomial.C (MIPRE.LowDegree.ofBool b)
• C.gateArith k (MIPRE.SAT.Gate.and u v) = MvPolynomial.X (Sum.inr u) * MvPolynomial.X (Sum.inr v)
• C.gateArith k (MIPRE.SAT.Gate.or u v) = 1 - (1 - MvPolynomial.X (Sum.inr u)) * (1 - MvPolynomial.X (Sum.inr v))
• C.gateArith k (MIPRE.SAT.Gate.not u) = 1 - MvPolynomial.X (Sum.inr u)

noncomputable def MIPRE.SAT.Circuit.consistencyFactor {F : Type u_1} [Field F] (C : Circuit) (k : ℕ) : MvPolynomial (ℕ ⊕ ℕ) F

The consistency factor for gate k.

Equations

• C.consistencyFactor k = 1 + MvPolynomial.X (Sum.inr k) + C.gateArith k (C.gates.getD k (MIPRE.SAT.Gate.const false))

noncomputable def MIPRE.SAT.Circuit.routedArith {F : Type u_1} [Field F] (C : Circuit) : MvPolynomial (ℕ ⊕ ℕ) F

All gate-consistency factors, together with the output literal.

Equations

• C.routedArith = (∏ k ∈ Finset.range C.size, C.consistencyFactor k) * MvPolynomial.X (Sum.inr (C.size - 1))

def MIPRE.SAT.Circuit.inputWeight (C : Circuit) (k : ℕ) (v : ℕ ⊕ ℕ) : ℕ

Contribution from an external-input copy link.

Equations

• C.inputWeight k v = match C.gates.getD k (MIPRE.SAT.Gate.const false) with | MIPRE.SAT.Gate.input i => if v = C.inputRef k i then 1 else 0 | x => 0

def MIPRE.SAT.Circuit.refWeight (g : Gate) : ℕ ⊕ ℕ → ℕ

Contribution from ordinary gate references, counting repeated references.

Equations

• MIPRE.SAT.Circuit.refWeight g (Sum.inl val) = 0
• MIPRE.SAT.Circuit.refWeight g (Sum.inr j) = List.count j g.refs

theorem MIPRE.SAT.Circuit.count_pair (u w j : ℕ) : List.count j [u, w] = (if j = u then 1 else 0) + if j = w then 1 else 0

theorem MIPRE.SAT.Circuit.degree_one_sub {F : Type u_1} [Field F] (p : MvPolynomial (ℕ ⊕ ℕ) F) (v : ℕ ⊕ ℕ) : MvPolynomial.degreeOf v (1 - p) ≤ MvPolynomial.degreeOf v p

theorem MIPRE.SAT.Circuit.degreeOf_gateArith {F : Type u_1} [Field F] (C : Circuit) (k : ℕ) (v : ℕ ⊕ ℕ) : MvPolynomial.degreeOf v (C.gateArith k (C.gates.getD k (Gate.const false))) ≤ C.inputWeight k v + refWeight (C.gates.getD k (Gate.const false)) v

theorem MIPRE.SAT.Circuit.degreeOf_consistencyFactor {F : Type u_1} [Field F] (C : Circuit) (k : ℕ) (v : ℕ ⊕ ℕ) : MvPolynomial.degreeOf v (C.consistencyFactor k) ≤ (if v = Sum.inr k then 1 else 0) + C.inputWeight k v + refWeight (C.gates.getD k (Gate.const false)) v

theorem MIPRE.SAT.Circuit.sum_inputWeight_le (C : Circuit) (v : ℕ ⊕ ℕ) : ∑ k ∈ Finset.range C.size, C.inputWeight k v ≤ 1

Copy routing contributes at most one occurrence of any variable.

theorem MIPRE.SAT.Circuit.sum_getD (l : List Gate) (f : Gate → ℕ) : ∑ k ∈ Finset.range l.length, f (l.getD k (Gate.const false)) = (List.map f l).sum

theorem MIPRE.SAT.Circuit.sum_refWeight (C : Circuit) (v : ℕ ⊕ ℕ) : ∑ k ∈ Finset.range C.size, refWeight (C.gates.getD k (Gate.const false)) v = match v with | Sum.inl val => 0 | Sum.inr j => C.fanout j

theorem MIPRE.SAT.Circuit.degreeOf_routedArith_le {F : Type u_1} [Field F] (C : Circuit) (hC : C.WellFormed) (v : ℕ ⊕ ℕ) : MvPolynomial.degreeOf v C.routedArith ≤ 5

A degree-five bound for the characteristic-two construction, stronger than the degree-six bound required by the PCP interface.

theorem MIPRE.SAT.Circuit.eval_gateArith {F : Type u_1} [Field F] (C : Circuit) (k : ℕ) (g : Gate) (x w : ℕ → Bool) (href : ∀ u ∈ g.refs, u < k) : (MvPolynomial.eval (Sum.elim (fun (i : ℕ) => LowDegree.ofBool (x i)) fun (j : ℕ) => LowDegree.ofBool (w j))) (C.gateArith k g) = LowDegree.ofBool (Gate.eval (fun (i : ℕ) => Sum.elim x w (C.inputRef k i)) (List.ofFn fun (j : Fin k) => w ↑j) g)

Boolean evaluation of a gate's polynomial.

theorem MIPRE.SAT.Circuit.eval_consistencyFactor {F : Type u_1} [Field F] [CharP F 2] (C : Circuit) (hC : C.WellFormed) (k : ℕ) (hk : k < C.size) (x w : ℕ → Bool) : (MvPolynomial.eval (Sum.elim (fun (i : ℕ) => LowDegree.ofBool (x i)) fun (j : ℕ) => LowDegree.ofBool (w j))) (C.consistencyFactor k) = if w k = Gate.eval (fun (i : ℕ) => Sum.elim x w (C.inputRef k i)) (List.ofFn fun (j : Fin k) => w ↑j) (C.gates.getD k (Gate.const false)) then 1 else 0

In characteristic two, the factor is exactly the Boolean consistency indicator.

theorem MIPRE.SAT.Circuit.eval_routedArith_iff {F : Type u_1} [Field F] [CharP F 2] (C : Circuit) (hC : C.WellFormed) (x w : ℕ → Bool) : (MvPolynomial.eval (Sum.elim (fun (i : ℕ) => LowDegree.ofBool (x i)) fun (j : ℕ) => LowDegree.ofBool (w j))) C.routedArith = 1 ↔ C.RoutedConsistent x w ∧ w (C.size - 1) = true

The polynomial is one precisely on consistent accepting Boolean assignments.

theorem MIPRE.SAT.Circuit.prod_zero_or_one {F : Type u_1} [Field F] {ι : Type u_2} (s : Finset ι) (f : ι → F) (h : ∀ i ∈ s, f i = 0 ∨ f i = 1) : ∏ i ∈ s, f i = 0 ∨ ∏ i ∈ s, f i = 1

theorem MIPRE.SAT.Circuit.eval_routedArith_bool {F : Type u_1} [Field F] [CharP F 2] (C : Circuit) (hC : C.WellFormed) (x w : ℕ → Bool) : (MvPolynomial.eval (Sum.elim (fun (i : ℕ) => LowDegree.ofBool (x i)) fun (j : ℕ) => LowDegree.ofBool (w j))) C.routedArith = 0 ∨ (MvPolynomial.eval (Sum.elim (fun (i : ℕ) => LowDegree.ofBool (x i)) fun (j : ℕ) => LowDegree.ofBool (w j))) C.routedArith = 1

Every Boolean assignment gives a Boolean field value, including rejected ones.