SafeDegree.lean

1 import CircuitObstructions.MultiplicativeDegree
2 
3 /-!
4 # Complete safe-degree bounds
5 
6 This module connects the exact polynomial representation to the C01 cover.
7 The complete-safe degree beta is defined as a least degree, not supplied as an
8 unproved numerical oracle. Affine output optimization is not in this block.
9 -/
10 namespace CircuitObstructions
11 
12 def CompleteSafeDegreeLE {n : Nat} (f : BFun n) (d : Nat) : Prop :=
13   ∀ v, f v = true → ∃ h : BFun n,
14     DegreeLE d h ∧ (∀ x, h x = true → f x = true) ∧ h v = true
15 
16 theorem CompleteSafeDegreeLE.mono {n d e : Nat} {f : BFun n}
17     (h : CompleteSafeDegreeLE f d) (hde : d ≤ e) : CompleteSafeDegreeLE f e := by
18   intro v hv
19   obtain ⟨g, hd, hs, hv'⟩ := h v hv
20   exact ⟨g, hd.mono hde, hs, hv'⟩
21 
22 theorem bprod_true_iff {W : Type} (l : List W) (s : State W) :
23     bprod l s = true ↔ ∀ i ∈ l, s i = true := by
24   induction l with
25   | nil => simp [bprod]
26   | cons i is ih => simp [bprod, ih]
27 
28 def pointIndicator {n : Nat} (v : Fin n → Bool) : BFun n :=
29   fun x => bprod (List.finRange n) (fun i => if v i then x i else ! x i)
30 
31 theorem pointIndicator_true_iff {n : Nat} (v x : Fin n → Bool) :
32     pointIndicator v x = true ↔ x = v := by
33   rw [pointIndicator, bprod_true_iff]
34   constructor
35   · intro h
36     funext i
37     have hi := h i (List.mem_finRange i)
38     cases hv : v i <;> cases hx : x i <;> simp_all
39   · intro hx
40     subst x
41     intro i _
42     cases v i <;> rfl
43 
44 theorem pointIndicator_degree {n : Nat} (v : Fin n → Bool) :
45     DegreeLE n (pointIndicator v) := by
46   have h := DegreeLE.product (List.finRange n)
47     (fun x i => if v i then x i else ! x i) (by
48       intro i
49       cases hv : v i
50       · exact (DegreeLE.variable i).not
51       · exact DegreeLE.variable i)
52   change DegreeLE n (fun x => bprod (List.finRange n)
53     (fun i => if v i then x i else ! x i))
54   simpa only [List.length_finRange] using h
55 
56 theorem completeSafeDegree_le_inputs {n : Nat} (f : BFun n) :
57     CompleteSafeDegreeLE f n := by
58   intro v hv
59   refine ⟨pointIndicator v, pointIndicator_degree v, ?_, ?_⟩
60   · intro x hx
61     rw [(pointIndicator_true_iff v x).mp hx]
62     exact hv
63   · exact (pointIndicator_true_iff v v).mpr rfl
64 
65 theorem exists_least_degree (P : Nat → Prop) (n : Nat) (hn : P n) :
66     ∃ r, P r ∧ ∀ k, P k → r ≤ k := by
67   classical
68   have h : ∀ n, P n → ∃ r, P r ∧ ∀ k, P k → r ≤ k := by
69     intro n
70     induction n using Nat.strongRecOn with
71     | ind n ih =>
72         intro hpn
73         by_cases he : ∃ k, k < n ∧ P k
74         · obtain ⟨k, hkn, hk⟩ := he
75           exact ih k hkn hk
76         · refine ⟨n, hpn, ?_⟩
77           intro k hk
78           by_cases hnle : n ≤ k
79           · exact hnle
80           · exact False.elim (he ⟨k, by omega, hk⟩)
81   exact h n hn
82 
83 theorem beta_exists {n : Nat} (f : BFun n) :
84     ∃ r, CompleteSafeDegreeLE f r ∧ ∀ k, CompleteSafeDegreeLE f k → r ≤ k := by
85   exact exists_least_degree (CompleteSafeDegreeLE f) n (completeSafeDegree_le_inputs f)
86 
87 noncomputable def beta {n : Nat} (f : BFun n) : Nat :=
88   Classical.choose (beta_exists f)
89 
90 theorem beta_spec {n : Nat} (f : BFun n) : CompleteSafeDegreeLE f (beta f) :=
91   (Classical.choose_spec (beta_exists f)).1
92 
93 theorem beta_le_of_cover {n d : Nat} {f : BFun n}
94     (h : CompleteSafeDegreeLE f d) : beta f ≤ d :=
95   (Classical.choose_spec (beta_exists f)).2 d h
96 
97 theorem beta_le_iff {n d : Nat} (f : BFun n) :
98     beta f ≤ d ↔ CompleteSafeDegreeLE f d := by
99   constructor
100   · exact (beta_spec f).mono
101   · exact beta_le_of_cover
102 
103 theorem beta_le_inputs {n : Nat} (f : BFun n) : beta f ≤ n :=
104   beta_le_of_cover (completeSafeDegree_le_inputs f)
105 
106 theorem beta_zero (n : Nat) : beta (n := n) (fun _ => false) = 0 := by
107   have h : CompleteSafeDegreeLE (n := n) (fun _ => false) 0 := by
108     intro v hv
109     cases hv
110   have hb := beta_le_of_cover h
111   omega
112 
113 theorem canonical_cut_completeSafeDegree (n a : Nat)
114     (p q : Circuit (CanonicalWire n a)) (f : BFun n)
115     (hR : Restores (canonicalBoundary n a) (p ++ q) f) :
116     CompleteSafeDegreeLE f (max (toffoliCount p) (toffoliCount q) + 1) := by
117   intro v hv
118   obtain ⟨i, hi⟩ := (cut_cover_complete (canonicalBoundary n a) p q f hR v).mp hv
119   refine ⟨fun x => packet (canonicalBoundary n a) p q x i,
120     canonical_cut_packet_degree n a p q i, ?_, hi⟩
121   intro x hx
122   exact cut_packet_safe (canonicalBoundary n a) p q f hR x i hx
123 
124 theorem Gate.toffoliCost_le_one {W : Type} (g : Gate W) : g.toffoliCost ≤ 1 := by
125   cases g <;> simp [Gate.toffoliCost]
126 
127 @[simp] theorem toffoliCount_nil {W : Type} : toffoliCount ([] : Circuit W) = 0 := rfl
128 
129 @[simp] theorem toffoliCount_cons {W : Type} (g : Gate W) (c : Circuit W) :
130     toffoliCount (g :: c) = g.toffoliCost + toffoliCount c := by
131   simp [toffoliCount]
132 
133 theorem exists_cut_with_toffoliCount {W : Type} (c : Circuit W)
134     (k : Nat) (hk : k ≤ toffoliCount c) :
135     ∃ p q : Circuit W, c = p ++ q ∧ toffoliCount p = k := by
136   induction c generalizing k with
137   | nil =>
138       have hk0 : k = 0 := by simp at hk; exact hk
139       subst k
140       exact ⟨[], [], rfl, rfl⟩
141   | cons g gs ih =>
142       by_cases hk0 : k = 0
143       · subst k
144         exact ⟨[], g :: gs, rfl, rfl⟩
145       · have hcost := Gate.toffoliCost_le_one g
146         have hk' : k - g.toffoliCost ≤ toffoliCount gs := by
147           simp only [toffoliCount_cons] at hk
148           omega
149         obtain ⟨p, q, hpq, hp⟩ := ih (k - g.toffoliCost) hk'
150         refine ⟨g :: p, q, ?_, ?_⟩
151         · simp [hpq]
152         · simp only [toffoliCount_cons, hp]
153           omega
154 
155 theorem exists_balanced_toffoli_cut {W : Type} (c : Circuit W) :
156     ∃ p q : Circuit W, c = p ++ q ∧
157       max (toffoliCount p) (toffoliCount q) ≤ (toffoliCount c + 1) / 2 := by
158   obtain ⟨p, q, hc, hp⟩ := exists_cut_with_toffoliCount c (toffoliCount c / 2)
159     (by omega)
160   refine ⟨p, q, hc, ?_⟩
161   have hsum : toffoliCount c = toffoliCount p + toffoliCount q := by
162     rw [hc, toffoliCount_append]
163   omega
164 
165 theorem canonical_restored_completeSafeDegree (n a : Nat)
166     (c : Circuit (CanonicalWire n a)) (f : BFun n)
167     (hR : Restores (canonicalBoundary n a) c f) :
168     CompleteSafeDegreeLE f ((toffoliCount c + 1) / 2 + 1) := by
169   obtain ⟨p, q, hc, hmax⟩ := exists_balanced_toffoli_cut c
170   have hR' : Restores (canonicalBoundary n a) (p ++ q) f := by rw [← hc]; exact hR
171   exact (canonical_cut_completeSafeDegree n a p q f hR').mono (by omega)
172 
173 theorem beta_le_half_toffoliCount (n a : Nat)
174     (c : Circuit (CanonicalWire n a)) (f : BFun n)
175     (hR : Restores (canonicalBoundary n a) c f) :
176     beta f ≤ (toffoliCount c + 1) / 2 + 1 := by
177   exact beta_le_of_cover (canonical_restored_completeSafeDegree n a c f hR)
178 
179 theorem beta_restoration_bound (n a : Nat)
180     (c : Circuit (CanonicalWire n a)) (f : BFun n)
181     (hR : Restores (canonicalBoundary n a) c f) :
182     2 * beta f ≤ toffoliCount c + 3 := by
183   have h := beta_le_half_toffoliCount n a c f hR
184   omega
185 
186 theorem toffoliCount_ge_two_beta_sub_three (n a : Nat)
187     (c : Circuit (CanonicalWire n a)) (f : BFun n)
188     (hR : Restores (canonicalBoundary n a) c f) :
189     2 * beta f - 3 ≤ toffoliCount c := by
190   have h := beta_restoration_bound n a c f hR
191   omega
192 
193 end CircuitObstructions

Back to source controls