SafeDegree: 22 declarations
On this page · Permalink · Source line 1173
L072 mono
On this page · Permalink · Source line 1175
Source. CircuitObstructions/SafeDegree.lean:16
Block. 02 Axioms. none
CircuitObstructions.CompleteSafeDegreeLE.mono {n d e : Nat} {f : CircuitObstructions.BFun n}
(h : CircuitObstructions.CompleteSafeDegreeLE f d) (hde : d ≤ e) : CircuitObstructions.CompleteSafeDegreeLE f eL073 bprod_true_iff
On this page · Permalink · Source line 1185
Source. CircuitObstructions/SafeDegree.lean:22
Block. 02 Axioms. propext, Quot.sound
CircuitObstructions.bprod_true_iff {W : Type} (l : List W) (s : CircuitObstructions.State W) :
CircuitObstructions.bprod l s = true ↔ ∀ (i : W), i ∈ l → s i = trueL074 pointIndicator_true_iff
On this page · Permalink · Source line 1195
Source. CircuitObstructions/SafeDegree.lean:31
Block. 02 Axioms. propext, Quot.sound
CircuitObstructions.pointIndicator_true_iff {n : Nat} (v x : Fin n → Bool) :
CircuitObstructions.pointIndicator v x = true ↔ x = vL075 pointIndicator_degree
On this page · Permalink · Source line 1205
Source. CircuitObstructions/SafeDegree.lean:44
Block. 02 Axioms. propext, Quot.sound
CircuitObstructions.pointIndicator_degree {n : Nat} (v : Fin n → Bool) :
CircuitObstructions.DegreeLE n (CircuitObstructions.pointIndicator v)L076 completeSafeDegree_le_inputs
On this page · Permalink · Source line 1215
Source. CircuitObstructions/SafeDegree.lean:56
Block. 02 Axioms. propext, Quot.sound
CircuitObstructions.completeSafeDegree_le_inputs {n : Nat} (f : CircuitObstructions.BFun n) :
CircuitObstructions.CompleteSafeDegreeLE f nL077 exists_least_degree
On this page · Permalink · Source line 1225
Source. CircuitObstructions/SafeDegree.lean:65
Block. 02 Axioms. propext, Classical.choice, Quot.sound
CircuitObstructions.exists_least_degree (P : Nat → Prop) (n : Nat) (hn : P n) : ∃ r, P r ∧ ∀ (k : Nat), P k → r ≤ kL078 beta_exists
On this page · Permalink · Source line 1234
Source. CircuitObstructions/SafeDegree.lean:83
Block. 02 Axioms. propext, Classical.choice, Quot.sound
CircuitObstructions.beta_exists {n : Nat} (f : CircuitObstructions.BFun n) :
∃ r, CircuitObstructions.CompleteSafeDegreeLE f r ∧ ∀ (k : Nat), CircuitObstructions.CompleteSafeDegreeLE f k → r ≤ kL079 beta_spec
On this page · Permalink · Source line 1244
Source. CircuitObstructions/SafeDegree.lean:90
Block. 02 Axioms. propext, Classical.choice, Quot.sound
CircuitObstructions.beta_spec {n : Nat} (f : CircuitObstructions.BFun n) :
CircuitObstructions.CompleteSafeDegreeLE f (CircuitObstructions.beta f)L080 beta_le_of_cover
On this page · Permalink · Source line 1254
Source. CircuitObstructions/SafeDegree.lean:93
Block. 02 Axioms. propext, Classical.choice, Quot.sound
CircuitObstructions.beta_le_of_cover {n d : Nat} {f : CircuitObstructions.BFun n}
(h : CircuitObstructions.CompleteSafeDegreeLE f d) : CircuitObstructions.beta f ≤ dL081 beta_le_iff
On this page · Permalink · Source line 1264
Source. CircuitObstructions/SafeDegree.lean:97
Block. 02 Axioms. propext, Classical.choice, Quot.sound
CircuitObstructions.beta_le_iff {n d : Nat} (f : CircuitObstructions.BFun n) :
CircuitObstructions.beta f ≤ d ↔ CircuitObstructions.CompleteSafeDegreeLE f dL082 beta_le_inputs
On this page · Permalink · Source line 1274
Source. CircuitObstructions/SafeDegree.lean:103
Block. 02 Axioms. propext, Classical.choice, Quot.sound
CircuitObstructions.beta_le_inputs {n : Nat} (f : CircuitObstructions.BFun n) : CircuitObstructions.beta f ≤ nL083 beta_zero
On this page · Permalink · Source line 1283
Source. CircuitObstructions/SafeDegree.lean:106
Block. 02 Axioms. propext, Classical.choice, Quot.sound
CircuitObstructions.beta_zero (n : Nat) : (CircuitObstructions.beta fun x => false) = 0L084 canonical_cut_completeSafeDegree
On this page · Permalink · Source line 1292
Source. CircuitObstructions/SafeDegree.lean:113
Block. 02 Axioms. propext, Classical.choice, Quot.sound
CircuitObstructions.canonical_cut_completeSafeDegree (n a : Nat)
(p q : CircuitObstructions.Circuit (CircuitObstructions.CanonicalWire n a)) (f : CircuitObstructions.BFun n)
(hR : CircuitObstructions.Restores (CircuitObstructions.canonicalBoundary n a) (p ++ q) f) :
CircuitObstructions.CompleteSafeDegreeLE f
(max (CircuitObstructions.toffoliCount p) (CircuitObstructions.toffoliCount q) + 1)L085 toffoliCost_le_one
On this page · Permalink · Source line 1305
Source. CircuitObstructions/SafeDegree.lean:124
Block. 02 Axioms. propext, Quot.sound
CircuitObstructions.Gate.toffoliCost_le_one {W : Type} (g : CircuitObstructions.Gate W) : g.toffoliCost ≤ 1L086 toffoliCount_nil
On this page · Permalink · Source line 1314
Source. CircuitObstructions/SafeDegree.lean:127
Block. 02 Axioms. propext
CircuitObstructions.toffoliCount_nil {W : Type} : CircuitObstructions.toffoliCount [] = 0L087 toffoliCount_cons
On this page · Permalink · Source line 1323
Source. CircuitObstructions/SafeDegree.lean:129
Block. 02 Axioms. propext
CircuitObstructions.toffoliCount_cons {W : Type} (g : CircuitObstructions.Gate W) (c : CircuitObstructions.Circuit W) :
CircuitObstructions.toffoliCount (g :: c) = g.toffoliCost + CircuitObstructions.toffoliCount cL088 exists_cut_with_toffoliCount
On this page · Permalink · Source line 1333
Source. CircuitObstructions/SafeDegree.lean:133
Block. 02 Axioms. propext, Quot.sound
CircuitObstructions.exists_cut_with_toffoliCount {W : Type} (c : CircuitObstructions.Circuit W) (k : Nat)
(hk : k ≤ CircuitObstructions.toffoliCount c) : ∃ p q, c = p ++ q ∧ CircuitObstructions.toffoliCount p = kL089 exists_balanced_toffoli_cut
On this page · Permalink · Source line 1343
Source. CircuitObstructions/SafeDegree.lean:155
Block. 02 Axioms. propext, Quot.sound
CircuitObstructions.exists_balanced_toffoli_cut {W : Type} (c : CircuitObstructions.Circuit W) :
∃ p q,
c = p ++ q ∧
max (CircuitObstructions.toffoliCount p) (CircuitObstructions.toffoliCount q) ≤
(CircuitObstructions.toffoliCount c + 1) / 2L090 canonical_restored_completeSafeDegree
On this page · Permalink · Source line 1356
Source. CircuitObstructions/SafeDegree.lean:165
Block. 02 Axioms. propext, Classical.choice, Quot.sound
CircuitObstructions.canonical_restored_completeSafeDegree (n a : Nat)
(c : CircuitObstructions.Circuit (CircuitObstructions.CanonicalWire n a)) (f : CircuitObstructions.BFun n)
(hR : CircuitObstructions.Restores (CircuitObstructions.canonicalBoundary n a) c f) :
CircuitObstructions.CompleteSafeDegreeLE f ((CircuitObstructions.toffoliCount c + 1) / 2 + 1)L091 beta_le_half_toffoliCount
On this page · Permalink · Source line 1368
Source. CircuitObstructions/SafeDegree.lean:173
Block. 02 Axioms. propext, Classical.choice, Quot.sound
CircuitObstructions.beta_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.beta f ≤ (CircuitObstructions.toffoliCount c + 1) / 2 + 1L092 beta_restoration_bound
On this page · Permalink · Source line 1380
Source. CircuitObstructions/SafeDegree.lean:179
Block. 02 Axioms. propext, Classical.choice, Quot.sound
CircuitObstructions.beta_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.beta f ≤ CircuitObstructions.toffoliCount c + 3L093 toffoliCount_ge_two_beta_sub_three
On this page · Permalink · Source line 1392
Source. CircuitObstructions/SafeDegree.lean:186
Block. 02 Axioms. propext, Classical.choice, Quot.sound
CircuitObstructions.toffoliCount_ge_two_beta_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.beta f - 3 ≤ CircuitObstructions.toffoliCount c