CutComparison: 13 declarations
On this page · Permalink · Source line 565
L017 target_separated
On this page · Permalink · Source line 567
Source. CircuitObstructions/CutComparison.lean:17
Block. 01 Axioms. propext
CircuitObstructions.Boundary.target_separated {X W : Type} (e : CircuitObstructions.Boundary X W) (x : X) :
e.encode x false ≠ e.encode x trueL018 canonical_input
On this page · Permalink · Source line 577
Source. CircuitObstructions/CutComparison.lean:39
Block. 01 Axioms. none
CircuitObstructions.canonical_input (n a : Nat) (x : Fin n → Bool) (b : Bool) (i : Fin n) :
(CircuitObstructions.canonicalBoundary n a).encode x b (Sum.inl i) = x iL019 canonical_ancilla
On this page · Permalink · Source line 587
Source. CircuitObstructions/CutComparison.lean:42
Block. 01 Axioms. none
CircuitObstructions.canonical_ancilla (n a : Nat) (x : Fin n → Bool) (b : Bool) (i : Fin a) :
(CircuitObstructions.canonicalBoundary n a).encode x b (Sum.inr (Sum.inl i)) = falseL020 canonical_target
On this page · Permalink · Source line 597
Source. CircuitObstructions/CutComparison.lean:45
Block. 01 Axioms. none
CircuitObstructions.canonical_target (n a : Nat) (x : Fin n → Bool) (b : Bool) :
(CircuitObstructions.canonicalBoundary n a).encode x b (Sum.inr (Sum.inr ())) = bL021 inverse_suffix_boundary
On this page · Permalink · Source line 607
Source. CircuitObstructions/CutComparison.lean:49
Block. 01 Axioms. propext, Quot.sound
CircuitObstructions.inverse_suffix_boundary {X W : Type} [DecidableEq W] (e : CircuitObstructions.Boundary X W)
(p q : CircuitObstructions.Circuit W) (f : X → Bool) (hR : CircuitObstructions.Restores e (p ++ q) f) (x : X)
(b : Bool) :
CircuitObstructions.run (List.reverse q) (e.encode x b) = CircuitObstructions.run p (e.encode x (b ^^ f x))L022 direction_nonzero
On this page · Permalink · Source line 619
Source. CircuitObstructions/CutComparison.lean:67
Block. 01 Axioms. propext, Classical.choice, Quot.sound
CircuitObstructions.direction_nonzero {X W : Type} [DecidableEq W] (e : CircuitObstructions.Boundary X W)
(p : CircuitObstructions.Circuit W) (x : X) : ∃ i, CircuitObstructions.direction e p x i = trueL023 cut_transport_identity
On this page · Permalink · Source line 629
Source. CircuitObstructions/CutComparison.lean:82
Block. 01 Axioms. propext, Quot.sound
CircuitObstructions.cut_transport_identity {X W : Type} [DecidableEq W] (e : CircuitObstructions.Boundary X W)
(p q : CircuitObstructions.Circuit W) (f : X → Bool) (hR : CircuitObstructions.Restores e (p ++ q) f) (x : X)
(i : W) : CircuitObstructions.packet e p q x i = (f x && CircuitObstructions.direction e p x i)L024 cut_packet_safe
On this page · Permalink · Source line 640
Source. CircuitObstructions/CutComparison.lean:91
Block. 01 Axioms. propext, Quot.sound
CircuitObstructions.cut_packet_safe {X W : Type} [DecidableEq W] (e : CircuitObstructions.Boundary X W)
(p q : CircuitObstructions.Circuit W) (f : X → Bool) (hR : CircuitObstructions.Restores e (p ++ q) f) (x : X)
(i : W) : CircuitObstructions.packet e p q x i = true → f x = trueL025 cut_cover_complete
On this page · Permalink · Source line 651
Source. CircuitObstructions/CutComparison.lean:99
Block. 01 Axioms. propext, Classical.choice, Quot.sound
CircuitObstructions.cut_cover_complete {X W : Type} [DecidableEq W] (e : CircuitObstructions.Boundary X W)
(p q : CircuitObstructions.Circuit W) (f : X → Bool) (hR : CircuitObstructions.Restores e (p ++ q) f) (x : X) :
f x = true ↔ ∃ i, CircuitObstructions.packet e p q x i = trueL026 complete_safe_cover
On this page · Permalink · Source line 662
Source. CircuitObstructions/CutComparison.lean:111
Block. 01 Axioms. propext, Classical.choice, Quot.sound
CircuitObstructions.complete_safe_cover {X W : Type} [DecidableEq W] (e : CircuitObstructions.Boundary X W)
(p q : CircuitObstructions.Circuit W) (f : X → Bool) (hR : CircuitObstructions.Restores e (p ++ q) f) :
(∀ (x : X) (i : W), CircuitObstructions.packet e p q x i = true → f x = true) ∧
∀ (x : X), f x = true ↔ ∃ i, CircuitObstructions.packet e p q x i = trueL027 cut_states_equal_iff_reject
On this page · Permalink · Source line 674
Source. CircuitObstructions/CutComparison.lean:119
Block. 01 Axioms. propext, Quot.sound
CircuitObstructions.cut_states_equal_iff_reject {X W : Type} [DecidableEq W] (e : CircuitObstructions.Boundary X W)
(p q : CircuitObstructions.Circuit W) (f : X → Bool) (hR : CircuitObstructions.Restores e (p ++ q) f) (x : X) :
CircuitObstructions.run p (e.encode x false) = CircuitObstructions.run (List.reverse q) (e.encode x false) ↔
f x = falseL028 every_index_cut
On this page · Permalink · Source line 686
Source. CircuitObstructions/CutComparison.lean:131
Block. 01 Axioms. propext, Classical.choice, Quot.sound
CircuitObstructions.every_index_cut {X W : Type} [DecidableEq W] (e : CircuitObstructions.Boundary X W)
(c : CircuitObstructions.Circuit W) (f : X → Bool) (hR : CircuitObstructions.Restores e c f) (k : Nat) (x : X) :
f x = true ↔ ∃ i, CircuitObstructions.packet e (List.take k c) (List.drop k c) x i = trueL029 canonical_complete_safe_cover
On this page · Permalink · Source line 697
Source. CircuitObstructions/CutComparison.lean:139
Block. 01 Axioms. propext, Classical.choice, Quot.sound
CircuitObstructions.canonical_complete_safe_cover (n a : Nat)
(c : CircuitObstructions.Circuit (CircuitObstructions.CanonicalWire n a)) (f : (Fin n → Bool) → Bool)
(hR : CircuitObstructions.Restores (CircuitObstructions.canonicalBoundary n a) c f) (k : Nat) :
(∀ (x : Fin n → Bool) (i : CircuitObstructions.CanonicalWire n a),
CircuitObstructions.packet (CircuitObstructions.canonicalBoundary n a) (List.take k c) (List.drop k c) x i =
true →
f x = true) ∧
∀ (x : Fin n → Bool),
f x = true ↔
∃ i,
CircuitObstructions.packet (CircuitObstructions.canonicalBoundary n a) (List.take k c) (List.drop k c) x i =
true