AffineOutput: 14 declarations
On this page · Permalink · Source line 1403
L094 restores_append
On this page · Permalink · Source line 1405
Source. CircuitObstructions/AffineOutput.lean:12
Block. 02 Axioms. propext
CircuitObstructions.restores_append {X W : Type} [DecidableEq W] (e : CircuitObstructions.Boundary X W)
(c d : CircuitObstructions.Circuit W) (f g : X → Bool) (hc : CircuitObstructions.Restores e c f)
(hd : CircuitObstructions.Restores e d g) : CircuitObstructions.Restores e (c ++ d) fun x => f x ^^ g xL095 canonical_target_not
On this page · Permalink · Source line 1416
Source. CircuitObstructions/AffineOutput.lean:20
Block. 02 Axioms. propext, Quot.sound
CircuitObstructions.canonical_target_not (n a : Nat) (x : Fin n → Bool) (b : Bool) :
(CircuitObstructions.Gate.not (CircuitObstructions.canonicalBoundary n a).target).eval
((CircuitObstructions.canonicalBoundary n a).encode x b) =
(CircuitObstructions.canonicalBoundary n a).encode x (b ^^ true)L096 canonical_input_to_target
On this page · Permalink · Source line 1428
Source. CircuitObstructions/AffineOutput.lean:34
Block. 02 Axioms. propext, Quot.sound
CircuitObstructions.canonical_input_to_target (n a : Nat) (i : Fin n) (x : Fin n → Bool) (b : Bool) :
(CircuitObstructions.inputToTarget n a i).eval ((CircuitObstructions.canonicalBoundary n a).encode x b) =
(CircuitObstructions.canonicalBoundary n a).encode x (b ^^ x i)L097 affine_restored_exists
On this page · Permalink · Source line 1439
Source. CircuitObstructions/AffineOutput.lean:45
Block. 02 Axioms. propext, Quot.sound
CircuitObstructions.affine_restored_exists (n a : Nat) (g : CircuitObstructions.BFun n)
(hg : CircuitObstructions.DegreeLE 1 g) :
∃ d,
CircuitObstructions.toffoliCount d = 0 ∧
CircuitObstructions.Restores (CircuitObstructions.canonicalBoundary n a) d gL098 betaStar_exists
On this page · Permalink · Source line 1452
Source. CircuitObstructions/AffineOutput.lean:76
Block. 02 Axioms. propext, Classical.choice, Quot.sound
CircuitObstructions.betaStar_exists {n : Nat} (f : CircuitObstructions.BFun n) :
∃ r, CircuitObstructions.AffineSafeDegreeLE f r ∧ ∀ (k : Nat), CircuitObstructions.AffineSafeDegreeLE f k → r ≤ kL099 betaStar_spec
On this page · Permalink · Source line 1462
Source. CircuitObstructions/AffineOutput.lean:85
Block. 02 Axioms. propext, Classical.choice, Quot.sound
CircuitObstructions.betaStar_spec {n : Nat} (f : CircuitObstructions.BFun n) :
CircuitObstructions.AffineSafeDegreeLE f (CircuitObstructions.betaStar f)L100 betaStar_le_of_bound
On this page · Permalink · Source line 1472
Source. CircuitObstructions/AffineOutput.lean:88
Block. 02 Axioms. propext, Classical.choice, Quot.sound
CircuitObstructions.betaStar_le_of_bound {n d : Nat} {f : CircuitObstructions.BFun n}
(h : CircuitObstructions.AffineSafeDegreeLE f d) : CircuitObstructions.betaStar f ≤ dL101 betaStar_le_inputs
On this page · Permalink · Source line 1482
Source. CircuitObstructions/AffineOutput.lean:92
Block. 02 Axioms. propext, Classical.choice, Quot.sound
CircuitObstructions.betaStar_le_inputs {n : Nat} (f : CircuitObstructions.BFun n) : CircuitObstructions.betaStar f ≤ nL102 beta_le_betaStar
On this page · Permalink · Source line 1491
Source. CircuitObstructions/AffineOutput.lean:97
Block. 02 Axioms. propext, Classical.choice, Quot.sound
CircuitObstructions.beta_le_betaStar {n : Nat} (f : CircuitObstructions.BFun n) :
CircuitObstructions.beta f ≤ CircuitObstructions.betaStar fL103 betaStar_le_half_toffoliCount
On this page · Permalink · Source line 1501
Source. CircuitObstructions/AffineOutput.lean:101
Block. 02 Axioms. propext, Classical.choice, Quot.sound
CircuitObstructions.betaStar_le_half_toffoliCount (n a : Nat)
(c : CircuitObstructions.Circuit (CircuitObstructions.CanonicalWire n a)) (f : CircuitObstructions.BFun n)
(hR : CircuitObstructions.Restores (CircuitObstructions.canonicalBoundary n a) c f) :
CircuitObstructions.betaStar f ≤ (CircuitObstructions.toffoliCount c + 1) / 2 + 1L104 betaStar_restoration_bound
On this page · Permalink · Source line 1513
Source. CircuitObstructions/AffineOutput.lean:112
Block. 02 Axioms. propext, Classical.choice, Quot.sound
CircuitObstructions.betaStar_restoration_bound (n a : Nat)
(c : CircuitObstructions.Circuit (CircuitObstructions.CanonicalWire n a)) (f : CircuitObstructions.BFun n)
(hR : CircuitObstructions.Restores (CircuitObstructions.canonicalBoundary n a) c f) :
2 * CircuitObstructions.betaStar f ≤ CircuitObstructions.toffoliCount c + 3L105 toffoliCount_ge_two_betaStar_sub_three
On this page · Permalink · Source line 1525
Source. CircuitObstructions/AffineOutput.lean:119
Block. 02 Axioms. propext, Classical.choice, Quot.sound
CircuitObstructions.toffoliCount_ge_two_betaStar_sub_three (n a : Nat)
(c : CircuitObstructions.Circuit (CircuitObstructions.CanonicalWire n a)) (f : CircuitObstructions.BFun n)
(hR : CircuitObstructions.Restores (CircuitObstructions.canonicalBoundary n a) c f) :
2 * CircuitObstructions.betaStar f - 3 ≤ CircuitObstructions.toffoliCount cL106 canonical_restored_output_degree
On this page · Permalink · Source line 1537
Source. CircuitObstructions/AffineOutput.lean:126
Block. 02 Axioms. propext, Quot.sound
CircuitObstructions.canonical_restored_output_degree (n a : Nat)
(c : CircuitObstructions.Circuit (CircuitObstructions.CanonicalWire n a)) (f : CircuitObstructions.BFun n)
(hR : CircuitObstructions.Restores (CircuitObstructions.canonicalBoundary n a) c f) :
CircuitObstructions.DegreeLE (CircuitObstructions.toffoliCount c + 1) fL107 restored_degree_and_cover_bound
On this page · Permalink · Source line 1549
Source. CircuitObstructions/AffineOutput.lean:140
Block. 02 Axioms. propext, Classical.choice, Quot.sound
CircuitObstructions.restored_degree_and_cover_bound (n a : Nat)
(c : CircuitObstructions.Circuit (CircuitObstructions.CanonicalWire n a)) (f : CircuitObstructions.BFun n)
(hR : CircuitObstructions.Restores (CircuitObstructions.canonicalBoundary n a) c f) :
CircuitObstructions.DegreeLE (CircuitObstructions.toffoliCount c + 1) f ∧
2 * CircuitObstructions.betaStar f ≤ CircuitObstructions.toffoliCount c + 3