DegreeChecks.lean

1 import CircuitObstructions.AffineOutput
2 
3 /-!
4 # Semantic controls for the new degree representation
5 
6 The lower-degree exclusions below are proved inside Lean. They are separate
7 from the independent finite truth-table checker shipped with this block.
8 -/
9 namespace CircuitObstructions
10 
11 def twoInput (a b : Bool) : Fin 2 → Bool := fun i => if i = 0 then a else b
12 
13 def squareParity (f : BFun 2) : Bool :=
14   Bool.xor (Bool.xor (f (twoInput false false)) (f (twoInput false true)))
15     (Bool.xor (f (twoInput true false)) (f (twoInput true true)))
16 
17 theorem squareParity_add (f g : BFun 2) :
18     squareParity (fun x => Bool.xor (f x) (g x)) =
19       Bool.xor (squareParity f) (squareParity g) := by
20   simp only [squareParity, Bool.xor_assoc, Bool.xor_left_comm, Bool.xor_comm]
21 
22 theorem affine_squareParity_zero (f : BFun 2) (h : DegreeLE 1 f) :
23     squareParity f = false := by
24   induction h with
25   | zero => rfl
26   | monomial l hl =>
27       cases l with
28       | nil => rfl
29       | cons i is =>
30           have his : is = [] := by cases is <;> simp_all
31           subst is
32           rcases i with ⟨i, hi⟩
33           have hx : i = 0 ∨ i = 1 := by omega
34           rcases hx with rfl | rfl <;> rfl
35   | add _ _ ihf ihg => rw [squareParity_add, ihf, ihg]; rfl
36 
37 def andTwo : BFun 2 := fun x => x 0 && x 1
38 
39 theorem andTwo_degree_two : DegreeLE 2 andTwo := by
40   change DegreeLE 2 (fun x => x 0 && x 1)
41   simpa [bprod] using DegreeLE.monomial (d := 2) [0,1] (by simp)
42 
43 theorem andTwo_not_affine : ¬ DegreeLE 1 andTwo := by
44   intro h
45   have hp := affine_squareParity_zero andTwo h
46   change true = false at hp
47   cases hp
48 
49 theorem andTwo_no_degree_one_safe_cover : ¬ CompleteSafeDegreeLE andTwo 1 := by
50   intro h
51   obtain ⟨g, hg, hs, hv⟩ := h (twoInput true true) (by decide)
52   have h00 : g (twoInput false false) = false := by
53     have hh := hs (twoInput false false)
54     cases he : g (twoInput false false) <;> simp_all [andTwo, twoInput]
55   have h01 : g (twoInput false true) = false := by
56     have hh := hs (twoInput false true)
57     cases he : g (twoInput false true) <;> simp_all [andTwo, twoInput]
58   have h10 : g (twoInput true false) = false := by
59     have hh := hs (twoInput true false)
60     cases he : g (twoInput true false) <;> simp_all [andTwo, twoInput]
61   have hp := affine_squareParity_zero g hg
62   simp [squareParity, h00, h01, h10, hv] at hp
63 
64 theorem beta_andTwo : beta andTwo = 2 := by
65   have hu := beta_le_inputs andTwo
66   have hn := andTwo_no_degree_one_safe_cover
67   have hl : ¬ beta andTwo ≤ 1 := by
68     intro h
69     exact hn ((beta_le_iff andTwo).mp h)
70   omega
71 
72 theorem betaStar_andTwo : betaStar andTwo = 2 := by
73   have hu := betaStar_le_inputs andTwo
74   have hl := beta_le_betaStar andTwo
75   rw [beta_andTwo] at hl
76   omega
77 
78 theorem restored_andTwo_needs_toffoli (a : Nat)
79     (c : Circuit (CanonicalWire 2 a))
80     (hR : Restores (canonicalBoundary 2 a) c andTwo) : 1 ≤ toffoliCount c := by
81   have h := betaStar_restoration_bound 2 a c andTwo hR
82   rw [betaStar_andTwo] at h
83   omega
84 
85 end CircuitObstructions

Back to source controls