AffineOutput.lean

1 import CircuitObstructions.SafeDegree
2 
3 /-!
4 # Zero-cost affine output changes and the optimized complete-cover bound
5 
6 An affine function is any function with a `DegreeLE 1` certificate. Every such
7 function is implemented by NOT/CNOT gates on the restored boundary. The proof
8 constructs a legal circuit and proves that its Toffoli count is zero.
9 -/
10 namespace CircuitObstructions
11 
12 theorem restores_append {X W : Type} [DecidableEq W] (e : Boundary X W)
13     (c d : Circuit W) (f g : X → Bool)
14     (hc : Restores e c f) (hd : Restores e d g) :
15     Restores e (c ++ d) (fun x => Bool.xor (f x) (g x)) := by
16   intro x b
17   rw [run_append, hc, hd]
18   simp only [Bool.xor_assoc]
19 
20 theorem canonical_target_not (n a : Nat) (x : Fin n → Bool) (b : Bool) :
21     (Gate.not (canonicalBoundary n a).target).eval ((canonicalBoundary n a).encode x b) =
22       (canonicalBoundary n a).encode x (Bool.xor b true) := by
23   funext i
24   cases i with
25   | inl j => simp [Gate.eval, write, canonicalBoundary]
26   | inr j =>
27       cases j with
28       | inl j => simp [Gate.eval, write, canonicalBoundary]
29       | inr j => simp [Gate.eval, write, canonicalBoundary]
30 
31 def inputToTarget (n a : Nat) (i : Fin n) : Gate (CanonicalWire n a) :=
32   .cnot (.inl i) (canonicalBoundary n a).target (by intro h; cases h)
33 
34 theorem canonical_input_to_target (n a : Nat) (i : Fin n) (x : Fin n → Bool) (b : Bool) :
35     (inputToTarget n a i).eval ((canonicalBoundary n a).encode x b) =
36       (canonicalBoundary n a).encode x (Bool.xor b (x i)) := by
37   funext j
38   cases j with
39   | inl j => simp [inputToTarget, Gate.eval, write, canonicalBoundary]
40   | inr j =>
41       cases j with
42       | inl j => simp [inputToTarget, Gate.eval, write, canonicalBoundary]
43       | inr j => simp [inputToTarget, Gate.eval, write, canonicalBoundary]
44 
45 theorem affine_restored_exists (n a : Nat) (g : BFun n) (hg : DegreeLE 1 g) :
46     ∃ d : Circuit (CanonicalWire n a), toffoliCount d = 0 ∧
47       Restores (canonicalBoundary n a) d g := by
48   induction hg with
49   | zero =>
50       refine ⟨[], rfl, ?_⟩
51       intro x b
52       simp
53   | monomial l hl =>
54       cases l with
55       | nil =>
56           refine ⟨[.not (canonicalBoundary n a).target], rfl, ?_⟩
57           intro x b
58           exact canonical_target_not n a x b
59       | cons i is =>
60           have his : is = [] := by
61             have hlen : is.length = 0 := by simp only [List.length_cons] at hl; omega
62             cases is <;> simp_all
63           subst is
64           refine ⟨[inputToTarget n a i], rfl, ?_⟩
65           intro x b
66           simpa [bprod] using canonical_input_to_target n a i x b
67   | add _ _ ihf ihg =>
68       obtain ⟨c, hc0, hc⟩ := ihf
69       obtain ⟨d, hd0, hd⟩ := ihg
70       exact ⟨c ++ d, by rw [toffoliCount_append, hc0, hd0],
71         restores_append (canonicalBoundary n a) c d _ _ hc hd⟩
72 
73 def AffineSafeDegreeLE {n : Nat} (f : BFun n) (d : Nat) : Prop :=
74   ∀ g : BFun n, DegreeLE 1 g → beta (fun x => Bool.xor (f x) (g x)) ≤ d
75 
76 theorem betaStar_exists {n : Nat} (f : BFun n) :
77     ∃ r, AffineSafeDegreeLE f r ∧ ∀ k, AffineSafeDegreeLE f k → r ≤ k := by
78   apply exists_least_degree (AffineSafeDegreeLE f) n
79   intro g _
80   exact beta_le_inputs _
81 
82 noncomputable def betaStar {n : Nat} (f : BFun n) : Nat :=
83   Classical.choose (betaStar_exists f)
84 
85 theorem betaStar_spec {n : Nat} (f : BFun n) : AffineSafeDegreeLE f (betaStar f) :=
86   (Classical.choose_spec (betaStar_exists f)).1
87 
88 theorem betaStar_le_of_bound {n d : Nat} {f : BFun n}
89     (h : AffineSafeDegreeLE f d) : betaStar f ≤ d :=
90   (Classical.choose_spec (betaStar_exists f)).2 d h
91 
92 theorem betaStar_le_inputs {n : Nat} (f : BFun n) : betaStar f ≤ n := by
93   apply betaStar_le_of_bound
94   intro g _
95   exact beta_le_inputs _
96 
97 theorem beta_le_betaStar {n : Nat} (f : BFun n) : beta f ≤ betaStar f := by
98   have h := betaStar_spec f (fun _ => false) DegreeLE.zero
99   simpa using h
100 
101 theorem betaStar_le_half_toffoliCount (n a : Nat)
102     (c : Circuit (CanonicalWire n a)) (f : BFun n)
103     (hR : Restores (canonicalBoundary n a) c f) :
104     betaStar f ≤ (toffoliCount c + 1) / 2 + 1 := by
105   apply betaStar_le_of_bound
106   intro g hg
107   obtain ⟨d, hd0, hd⟩ := affine_restored_exists n a g hg
108   have h := beta_le_half_toffoliCount n a (c ++ d) _
109     (restores_append (canonicalBoundary n a) c d f g hR hd)
110   simpa only [toffoliCount_append, hd0, Nat.add_zero] using h
111 
112 theorem betaStar_restoration_bound (n a : Nat)
113     (c : Circuit (CanonicalWire n a)) (f : BFun n)
114     (hR : Restores (canonicalBoundary n a) c f) :
115     2 * betaStar f ≤ toffoliCount c + 3 := by
116   have h := betaStar_le_half_toffoliCount n a c f hR
117   omega
118 
119 theorem toffoliCount_ge_two_betaStar_sub_three (n a : Nat)
120     (c : Circuit (CanonicalWire n a)) (f : BFun n)
121     (hR : Restores (canonicalBoundary n a) c f) :
122     2 * betaStar f - 3 ≤ toffoliCount c := by
123   have h := betaStar_restoration_bound n a c f hR
124   omega
125 
126 theorem canonical_restored_output_degree (n a : Nat)
127     (c : Circuit (CanonicalWire n a)) (f : BFun n)
128     (hR : Restores (canonicalBoundary n a) c f) :
129     DegreeLE (toffoliCount c + 1) f := by
130   have h := canonical_run_coordinate_degree n a c false (canonicalBoundary n a).target
131   have heq : (fun x => run c ((canonicalBoundary n a).encode x false)
132       (canonicalBoundary n a).target) = f := by
133     funext x
134     rw [hR x false, Boundary.target_eq]
135     simp
136   rw [heq] at h
137   exact h
138 
139 /-- Joint formal endpoint for the numerical and polynomial parts of C02. -/
140 theorem restored_degree_and_cover_bound (n a : Nat)
141     (c : Circuit (CanonicalWire n a)) (f : BFun n)
142     (hR : Restores (canonicalBoundary n a) c f) :
143     DegreeLE (toffoliCount c + 1) f ∧
144       2 * betaStar f ≤ toffoliCount c + 3 := by
145   exact ⟨canonical_restored_output_degree n a c f hR,
146     betaStar_restoration_bound n a c f hR⟩
147 
148 end CircuitObstructions

Back to source controls