OAI/Computability/QuantumFactoring/TensorWiring.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExactQuantumFactoring.tensorWire line 18
2. lemma OAI.ExactQuantumFactoring.tensorLayout_wire line 23
3. def OAI.ExactQuantumFactoring.tensorSelect line 36
4. lemma OAI.ExactQuantumFactoring.tensorSelect_eval line 38
5. lemma OAI.ExactQuantumFactoring.tensorSelect_inverse line 42
6. def OAI.ExactQuantumFactoring.tensorNetwork line 49

   Source documentation

   Direct concatenation prepares K fixed blocks. No branch-indexed truth table is allocated; the count is the sum of the supplied K finite networks.

   def tensorNetwork {n q : ℕ} : {K : ℕ} → (Fin K → BooleanNetwork n q) →
       BooleanNetwork n (tensorWidth q K)
     | 0,_ => select Fin.elim0
     | _K+1,f => (f 0).pair (tensorNetwork (fun i => f i.succ))

   Mentions: OAI.ExactQuantumFactoring.BooleanNetwork, OAI.ExactQuantumFactoring.tensorWidth

7. lemma OAI.ExactQuantumFactoring.tensorNetwork_eval line 53
8. lemma OAI.ExactQuantumFactoring.tensorNetwork_count line 58
9. lemma OAI.ExactQuantumFactoring.tensorNetwork_count_le line 63