Degree.lean

1 import CircuitObstructions.Gates
2 
3 /-!
4 # Boolean degree certificates
5 
6 `DegreeLE d f` says that f is an XOR of monomials of length at most d.
7 Repeated input variables are permitted in a representation. Their Boolean
8 idempotence can only lower multilinear degree. Zero has degree bound zero.
9 This is a semantic polynomial representation, not a syntactic circuit weight.
10 -/
11 namespace CircuitObstructions
12 
13 abbrev BFun (n : Nat) := (Fin n → Bool) → Bool
14 
15 def bprod {W : Type} : List W → State W → Bool
16   | [], _ => true
17   | i :: is, s => s i && bprod is s
18 
19 @[simp] theorem bprod_nil {W : Type} (s : State W) : bprod [] s = true := rfl
20 @[simp] theorem bprod_cons {W : Type} (i : W) (is : List W) (s : State W) :
21     bprod (i :: is) s = (s i && bprod is s) := rfl
22 
23 theorem bprod_append {W : Type} (l k : List W) (s : State W) :
24     bprod (l ++ k) s = (bprod l s && bprod k s) := by
25   induction l with
26   | nil => simp [bprod]
27   | cons i is ih => simp [bprod, ih, Bool.and_assoc]
28 
29 theorem xor_and_right (a b c : Bool) :
30     ((Bool.xor a b) && c) = Bool.xor (a && c) (b && c) := by
31   cases a <;> cases b <;> cases c <;> rfl
32 
33 theorem and_xor_right (a b c : Bool) :
34     (a && Bool.xor b c) = Bool.xor (a && b) (a && c) := by
35   cases a <;> cases b <;> cases c <;> rfl
36 
37 theorem not_as_xor_one (a : Bool) : (!a) = Bool.xor a true := by
38   cases a <;> rfl
39 
40 inductive DegreeLE {n : Nat} (d : Nat) : BFun n → Prop where
41   | zero : DegreeLE d (fun _ => false)
42   | monomial (l : List (Fin n)) (bound : l.length ≤ d) :
43       DegreeLE d (fun x => bprod l x)
44   | add {f g : BFun n} : DegreeLE d f → DegreeLE d g →
45       DegreeLE d (fun x => Bool.xor (f x) (g x))
46 
47 theorem DegreeLE.mono {n d e : Nat} {f : BFun n}
48     (h : DegreeLE d f) (hde : d ≤ e) : DegreeLE e f := by
49   induction h with
50   | zero => exact .zero
51   | monomial l hl => exact .monomial l (Nat.le_trans hl hde)
52   | add _ _ ihf ihg => exact .add ihf ihg
53 
54 theorem DegreeLE.one (n d : Nat) : DegreeLE (n := n) d (fun _ => true) := by
55   exact .monomial [] (Nat.zero_le d)
56 
57 theorem DegreeLE.constant (n d : Nat) (b : Bool) :
58     DegreeLE (n := n) d (fun _ => b) := by
59   cases b
60   · exact .zero
61   · exact DegreeLE.one n d
62 
63 theorem DegreeLE.variable {n : Nat} (i : Fin n) :
64     DegreeLE 1 (fun x => x i) := by
65   simpa using DegreeLE.monomial (d := 1) [i] (by simp)
66 
67 theorem DegreeLE.xor {n d e : Nat} {f g : BFun n}
68     (hf : DegreeLE d f) (hg : DegreeLE e g) :
69     DegreeLE (max d e) (fun x => Bool.xor (f x) (g x)) := by
70   exact .add (hf.mono (Nat.le_max_left d e)) (hg.mono (Nat.le_max_right d e))
71 
72 theorem DegreeLE.not {n d : Nat} {f : BFun n} (hf : DegreeLE d f) :
73     DegreeLE d (fun x => ! f x) := by
74   simpa only [not_as_xor_one] using DegreeLE.add hf (DegreeLE.one n d)
75 
76 theorem DegreeLE.monomial_mul {n d e : Nat} (l : List (Fin n)) (hl : l.length ≤ d)
77     {g : BFun n} (hg : DegreeLE e g) :
78     DegreeLE (d + e) (fun x => bprod l x && g x) := by
79   induction hg with
80   | zero => simpa using (DegreeLE.zero (n := n) (d := d + e))
81   | monomial k hk =>
82       have hlen : (l ++ k).length ≤ d + e := by simp only [List.length_append]; omega
83       simpa only [bprod_append] using DegreeLE.monomial (l ++ k) hlen
84   | add _ _ ihf ihg =>
85       simpa only [and_xor_right] using DegreeLE.add ihf ihg
86 
87 theorem DegreeLE.mul {n d e : Nat} {f g : BFun n}
88     (hf : DegreeLE d f) (hg : DegreeLE e g) :
89     DegreeLE (d + e) (fun x => f x && g x) := by
90   induction hf with
91   | zero => simpa using (DegreeLE.zero (n := n) (d := d + e))
92   | monomial l hl => exact DegreeLE.monomial_mul l hl hg
93   | add _ _ ihf ihg =>
94       simpa only [xor_and_right] using DegreeLE.add ihf ihg
95 
96 theorem DegreeLE.product {n : Nat} {W : Type} (l : List W) (s : (Fin n → Bool) → State W)
97     (h : ∀ i, DegreeLE 1 (fun x => s x i)) :
98     DegreeLE l.length (fun x => bprod l (s x)) := by
99   induction l with
100   | nil => exact DegreeLE.one n 0
101   | cons i is ih =>
102       simpa only [List.length_cons, bprod_cons, Nat.add_comm 1] using (h i).mul ih
103 
104 /-- A concrete XOR-list representation, retained for a direct polynomial witness. -/
105 def polyEval {n : Nat} : List (List (Fin n)) → BFun n
106   | [], _ => false
107   | l :: p, x => Bool.xor (bprod l x) (polyEval p x)
108 
109 theorem polyEval_append {n : Nat} (p q : List (List (Fin n))) (x : Fin n → Bool) :
110     polyEval (p ++ q) x = Bool.xor (polyEval p x) (polyEval q x) := by
111   induction p with
112   | nil => simp [polyEval]
113   | cons l ls ih => simp [polyEval, ih]
114 
115 theorem DegreeLE.polynomial_witness {n d : Nat} {f : BFun n} (h : DegreeLE d f) :
116     ∃ p : List (List (Fin n)), (∀ l ∈ p, l.length ≤ d) ∧ polyEval p = f := by
117   induction h with
118   | zero => exact ⟨[], by simp, rfl⟩
119   | monomial l hl =>
120       refine ⟨[l], by simpa using hl, ?_⟩
121       funext x
122       simp [polyEval]
123   | add _ _ ihf ihg =>
124       obtain ⟨p, hp, hpf⟩ := ihf
125       obtain ⟨q, hq, hqg⟩ := ihg
126       refine ⟨p ++ q, ?_, ?_⟩
127       · intro l hl
128         rcases List.mem_append.mp hl with hl | hl
129         · exact hp l hl
130         · exact hq l hl
131       · funext x
132         rw [polyEval_append, hpf, hqg]
133 
134 theorem polynomial_degree_certificate {n d : Nat} (p : List (List (Fin n)))
135     (hp : ∀ l ∈ p, l.length ≤ d) : DegreeLE d (polyEval p) := by
136   induction p with
137   | nil => exact .zero
138   | cons l ls ih =>
139       exact .add (.monomial l (hp l (by simp)))
140         (ih (fun k hk => hp k (by simp [hk])))
141 
142 theorem degreeLE_iff_polynomial {n d : Nat} (f : BFun n) :
143     DegreeLE d f ↔ ∃ p : List (List (Fin n)),
144       (∀ l ∈ p, l.length ≤ d) ∧ polyEval p = f := by
145   constructor
146   · exact DegreeLE.polynomial_witness
147   · rintro ⟨p, hp, rfl⟩
148     exact polynomial_degree_certificate p hp
149 
150 end CircuitObstructions

Back to source controls