OAI/Computability/QuantumFactoring/ClosedLevelCircuit.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExactQuantumFactoring.BitArithmetic.oddPartNet line 22

   Source documentation

   Compute the odd part by a bounded gcd and exact integer division.

   def oddPartNet {k n : ℕ} (a : BooleanNetwork k n) : BooleanNetwork k n :=
   …

   Mentions: OAI.ExactQuantumFactoring.BooleanNetwork

2. lemma OAI.ExactQuantumFactoring.BitArithmetic.oddPartNet_value line 25
3. def OAI.ExactQuantumFactoring.BitArithmetic.closedLevelNet line 40

   Source documentation

   An exact level count, selected by the bounded divisibility predicate. The branch at t≥n is zero since a is a nonzero n-bit word.

   def closedLevelNet {k n : ℕ} (a : BooleanNetwork k n) (t : ℕ) : BooleanNetwork k n :=
   …

   Mentions: OAI.ExactQuantumFactoring.BooleanNetwork

4. lemma OAI.ExactQuantumFactoring.BitArithmetic.closedLevelNet_value line 47
5. def OAI.ExactQuantumFactoring.BitArithmetic.oddPartBound line 79
6. lemma OAI.ExactQuantumFactoring.BitArithmetic.oddPartNet_count line 80
7. def OAI.ExactQuantumFactoring.BitArithmetic.closedLevelBound line 89
8. lemma OAI.ExactQuantumFactoring.BitArithmetic.closedLevelNet_count line 90