OAI/Computability/QuantumFactoring/TableTotientCircuit.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExactQuantumFactoring.BitArithmetic.totientFromList line 20

   Source documentation

   Run the polynomial accumulator scan from the queried word and one.

   def totientFromList {k w : ℕ} (v : BooleanNetwork k w) (qs : List (BooleanNetwork k w)) :
       BooleanNetwork k w :=
   …

   Mentions: OAI.ExactQuantumFactoring.BooleanNetwork

2. lemma OAI.ExactQuantumFactoring.BitArithmetic.totientFromList_value line 25
3. lemma OAI.ExactQuantumFactoring.BitArithmetic.totientFromList_count line 51
4. def OAI.ExactQuantumFactoring.BitArithmetic.tableTotient line 61

   Source documentation

   At most n repetitions of each rectangular prime entry suffice. Unlike order stripping, the totient accumulator does not need a wide product.

   def tableTotient {k n : ℕ} (v : BooleanNetwork k n)
       (rows : List (BooleanNetwork k n×List (BooleanNetwork k n))) : BooleanNetwork k n :=
   …

   Mentions: OAI.ExactQuantumFactoring.BooleanNetwork

5. theorem OAI.ExactQuantumFactoring.BitArithmetic.tableTotient_exact line 65
6. def OAI.ExactQuantumFactoring.BitArithmetic.tableTotientBound line 77
7. lemma OAI.ExactQuantumFactoring.BitArithmetic.tableTotient_count line 79