CutComparison.lean

1 import CircuitObstructions.Gates
2 
3 /-!
4 # Complete discrepancy covers (maintained claim C01)
5 
6 The endpoint condition is the definition of a restored implementation. It is not
7 an axiom. Reversibility is derived from the legal gates in `Gates.lean`.
8 -/
9 namespace CircuitObstructions
10 
11 /-- An encoding whose designated target really stores the supplied Boolean bit. -/
12 structure Boundary (X W : Type) where
13   encode : X → Bool → State W
14   target : W
15   target_eq : ∀ x b, encode x b target = b
16 
17 theorem Boundary.target_separated {X W : Type} (e : Boundary X W) (x : X) :
18     e.encode x false ≠ e.encode x true := by
19   intro h
20   have hh := congrArg (fun s : State W => s e.target) h
21   simp only [e.target_eq, Bool.false_eq_true] at hh
22 
23 /-- Correctness includes every logical input and both initial target values. -/
24 def Restores {X W : Type} [DecidableEq W] (e : Boundary X W)
25     (c : Circuit W) (f : X → Bool) : Prop :=
26   ∀ x b, run c (e.encode x b) = e.encode x (Bool.xor b (f x))
27 
28 /-- Explicit logical inputs, zero ancillas, and one target. -/
29 abbrev CanonicalWire (n a : Nat) := Sum (Fin n) (Sum (Fin a) Unit)
30 
31 def canonicalBoundary (n a : Nat) : Boundary (Fin n → Bool) (CanonicalWire n a) where
32   encode x b
33     | .inl i => x i
34     | .inr (.inl _) => false
35     | .inr (.inr _) => b
36   target := .inr (.inr ())
37   target_eq := by intros; rfl
38 
39 @[simp] theorem canonical_input (n a : Nat) (x : Fin n → Bool) (b : Bool) (i : Fin n) :
40     (canonicalBoundary n a).encode x b (.inl i) = x i := rfl
41 
42 @[simp] theorem canonical_ancilla (n a : Nat) (x : Fin n → Bool) (b : Bool) (i : Fin a) :
43     (canonicalBoundary n a).encode x b (.inr (.inl i)) = false := rfl
44 
45 @[simp] theorem canonical_target (n a : Nat) (x : Fin n → Bool) (b : Bool) :
46     (canonicalBoundary n a).encode x b (.inr (.inr ())) = b := rfl
47 
48 /-- The inverse suffix meets the forward prefix on the appropriate target branch. -/
49 theorem inverse_suffix_boundary {X W : Type} [DecidableEq W]
50     (e : Boundary X W) (p q : Circuit W) (f : X → Bool)
51     (hR : Restores e (p ++ q) f) (x : X) (b : Bool) :
52     run q.reverse (e.encode x b) = run p (e.encode x (Bool.xor b (f x))) := by
53   have h := hR x (Bool.xor b (f x))
54   rw [run_append, xor_cancel_right] at h
55   have hh := congrArg (run q.reverse) h
56   simpa only [run_reverse_run] using hh.symm
57 
58 def direction {X W : Type} [DecidableEq W] (e : Boundary X W)
59     (p : Circuit W) (x : X) (i : W) : Bool :=
60   Bool.xor (run p (e.encode x true) i) (run p (e.encode x false) i)
61 
62 def packet {X W : Type} [DecidableEq W] (e : Boundary X W)
63     (p q : Circuit W) (x : X) (i : W) : Bool :=
64   Bool.xor (run p (e.encode x false) i) (run q.reverse (e.encode x false) i)
65 
66 /-- Distinct initial target bits remain distinguishable after every prefix. -/
67 theorem direction_nonzero {X W : Type} [DecidableEq W]
68     (e : Boundary X W) (p : Circuit W) (x : X) :
69     ∃ i, direction e p x i = true := by
70   classical
71   apply Classical.byContradiction
72   intro h
73   have heq : run p (e.encode x false) = run p (e.encode x true) := by
74     funext i
75     have hn : ¬ direction e p x i = true := fun hi => h ⟨i, hi⟩
76     unfold direction at hn
77     cases ha : run p (e.encode x true) i <;>
78       cases hb : run p (e.encode x false) i <;> simp_all
79   exact e.target_separated x (run_injective p heq)
80 
81 /-- Exact pointwise transport identity H_i = f AND D_i. -/
82 theorem cut_transport_identity {X W : Type} [DecidableEq W]
83     (e : Boundary X W) (p q : Circuit W) (f : X → Bool)
84     (hR : Restores e (p ++ q) f) (x : X) (i : W) :
85     packet e p q x i = (f x && direction e p x i) := by
86   unfold packet
87   rw [inverse_suffix_boundary e p q f hR x false]
88   cases hf : f x <;> simp [direction, xor_commute]
89 
90 /-- Every discrepancy vanishes on every rejected input. -/
91 theorem cut_packet_safe {X W : Type} [DecidableEq W]
92     (e : Boundary X W) (p q : Circuit W) (f : X → Bool)
93     (hR : Restores e (p ++ q) f) (x : X) (i : W) :
94     packet e p q x i = true → f x = true := by
95   rw [cut_transport_identity e p q f hR]
96   cases f x <;> simp
97 
98 /-- Every accepted input is detected by at least one discrepancy coordinate. -/
99 theorem cut_cover_complete {X W : Type} [DecidableEq W]
100     (e : Boundary X W) (p q : Circuit W) (f : X → Bool)
101     (hR : Restores e (p ++ q) f) (x : X) :
102     f x = true ↔ ∃ i, packet e p q x i = true := by
103   constructor
104   · intro hf
105     obtain ⟨i, hi⟩ := direction_nonzero e p x
106     exact ⟨i, by rw [cut_transport_identity e p q f hR, hf, hi]; rfl⟩
107   · rintro ⟨i, hi⟩
108     exact cut_packet_safe e p q f hR x i hi
109 
110 /-- C01, packaged as simultaneous safety and completeness at an arbitrary cut. -/
111 theorem complete_safe_cover {X W : Type} [DecidableEq W]
112     (e : Boundary X W) (p q : Circuit W) (f : X → Bool)
113     (hR : Restores e (p ++ q) f) :
114     (∀ x i, packet e p q x i = true → f x = true) ∧
115     (∀ x, f x = true ↔ ∃ i, packet e p q x i = true) := by
116   exact ⟨cut_packet_safe e p q f hR, cut_cover_complete e p q f hR⟩
117 
118 /-- An equivalent register-equality characterization, with no chosen decoder. -/
119 theorem cut_states_equal_iff_reject {X W : Type} [DecidableEq W]
120     (e : Boundary X W) (p q : Circuit W) (f : X → Bool)
121     (hR : Restores e (p ++ q) f) (x : X) :
122     run p (e.encode x false) = run q.reverse (e.encode x false) ↔ f x = false := by
123   rw [inverse_suffix_boundary e p q f hR x false]
124   cases hf : f x
125   · simp
126   · simp only [Bool.false_xor, Bool.true_eq_false, iff_false]
127     intro h
128     exact e.target_separated x (run_injective p h)
129 
130 /-- The theorem applies to every index, not only a cut supplied as a decomposition. -/
131 theorem every_index_cut {X W : Type} [DecidableEq W]
132     (e : Boundary X W) (c : Circuit W) (f : X → Bool)
133     (hR : Restores e c f) (k : Nat) (x : X) :
134     f x = true ↔ ∃ i, packet e (c.take k) (c.drop k) x i = true := by
135   apply cut_cover_complete e (c.take k) (c.drop k) f
136   simpa only [List.take_append_drop] using hR
137 
138 /-- Specialization to arbitrary finite logical registers and zero-initialized workspace. -/
139 theorem canonical_complete_safe_cover (n a : Nat)
140     (c : Circuit (CanonicalWire n a)) (f : (Fin n → Bool) → Bool)
141     (hR : Restores (canonicalBoundary n a) c f) (k : Nat) :
142     (∀ x i, packet (canonicalBoundary n a) (c.take k) (c.drop k) x i = true →
143       f x = true) ∧
144     (∀ x, f x = true ↔
145       ∃ i, packet (canonicalBoundary n a) (c.take k) (c.drop k) x i = true) := by
146   apply complete_safe_cover (canonicalBoundary n a) (c.take k) (c.drop k) f
147   simpa only [List.take_append_drop] using hR
148 
149 end CircuitObstructions

Back to source controls