MultiplicativeDegree: 12 declarations

CircuitObstructions.withoutWire_length_le {W : Type} [DecidableEq W] (l : List W) (t : W) :
  (CircuitObstructions.withoutWire l t).length ≤ l.length

Permalink · Source line 1040

CircuitObstructions.withoutWire_length_lt {W : Type} [DecidableEq W] (l : List W) (t : W) (ht : t ∈ l) :
  (CircuitObstructions.withoutWire l t).length + 1 ≤ l.length

Permalink · Source line 1050

CircuitObstructions.bprod_write {W : Type} [DecidableEq W] (l : List W) (s : CircuitObstructions.State W) (t : W)
  (b : Bool) :
  CircuitObstructions.bprod l (CircuitObstructions.write s t b) =
    ((if t ∈ l then b else true) && CircuitObstructions.bprod (CircuitObstructions.withoutWire l t) s)

Permalink · Source line 1060

CircuitObstructions.bprod_write_absent {W : Type} [DecidableEq W] (l : List W) (s : CircuitObstructions.State W) (t : W)
  (b : Bool) (ht : ¬t ∈ l) :
  CircuitObstructions.bprod l (CircuitObstructions.write s t b) = CircuitObstructions.bprod l s

Permalink · Source line 1072

CircuitObstructions.workspaceDegree_initial {n : Nat} {W : Type} (s : (Fin n → Bool) → CircuitObstructions.State W)
  (h : ∀ (i : W), CircuitObstructions.DegreeLE 1 fun x => s x i) : CircuitObstructions.WorkspaceDegree s 0

Permalink · Source line 1083

CircuitObstructions.workspaceDegree_toggle {n : Nat} {W : Type} [DecidableEq W]
  (s : (Fin n → Bool) → CircuitObstructions.State W) (t : W) (controls : List W) (k : Nat)
  (h : CircuitObstructions.WorkspaceDegree s k) :
  CircuitObstructions.WorkspaceDegree (CircuitObstructions.toggleProduct s t controls) (k + (controls.length - 1))

Permalink · Source line 1093

CircuitObstructions.workspaceDegree_gate {n : Nat} {W : Type} [DecidableEq W]
  (s : (Fin n → Bool) → CircuitObstructions.State W) (g : CircuitObstructions.Gate W) (k : Nat)
  (h : CircuitObstructions.WorkspaceDegree s k) :
  CircuitObstructions.WorkspaceDegree (fun x => g.eval (s x)) (k + g.toffoliCost)

Permalink · Source line 1105

CircuitObstructions.workspaceDegree_run {n : Nat} {W : Type} [DecidableEq W] (c : CircuitObstructions.Circuit W)
  (s : (Fin n → Bool) → CircuitObstructions.State W) (k : Nat) (h : CircuitObstructions.WorkspaceDegree s k) :
  CircuitObstructions.WorkspaceDegree (fun x => CircuitObstructions.run c (s x))
    (k + CircuitObstructions.toffoliCount c)

Permalink · Source line 1117

CircuitObstructions.run_coordinate_degree {n : Nat} {W : Type} [DecidableEq W] (c : CircuitObstructions.Circuit W)
  (s : (Fin n → Bool) → CircuitObstructions.State W) (hs : ∀ (i : W), CircuitObstructions.DegreeLE 1 fun x => s x i)
  (i : W) :
  CircuitObstructions.DegreeLE (CircuitObstructions.toffoliCount c + 1) fun x => CircuitObstructions.run c (s x) i

Permalink · Source line 1129

CircuitObstructions.canonical_boundary_degree (n a : Nat) (b : Bool) (i : CircuitObstructions.CanonicalWire n a) :
  CircuitObstructions.DegreeLE 1 fun x => (CircuitObstructions.canonicalBoundary n a).encode x b i

Permalink · Source line 1141

CircuitObstructions.canonical_run_coordinate_degree (n a : Nat)
  (c : CircuitObstructions.Circuit (CircuitObstructions.CanonicalWire n a)) (b : Bool)
  (i : CircuitObstructions.CanonicalWire n a) :
  CircuitObstructions.DegreeLE (CircuitObstructions.toffoliCount c + 1) fun x =>
    CircuitObstructions.run c ((CircuitObstructions.canonicalBoundary n a).encode x b) i

Permalink · Source line 1151

CircuitObstructions.canonical_cut_packet_degree (n a : Nat)
  (p q : CircuitObstructions.Circuit (CircuitObstructions.CanonicalWire n a))
  (i : CircuitObstructions.CanonicalWire n a) :
  CircuitObstructions.DegreeLE (max (CircuitObstructions.toffoliCount p) (CircuitObstructions.toffoliCount q) + 1)
    fun x => CircuitObstructions.packet (CircuitObstructions.canonicalBoundary n a) p q x i

Permalink · Source line 1164