OAI/Computability/QuantumFactoring/RetainedTable.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExactQuantumFactoring.NodeMachine.fieldRows line 23

   Source documentation

   Every field is selected from its actual retained location. Dummy rows are kept: the rectangular shape is a compile-time function only of n and t.

   def fieldRows (t : ℕ) : List (BooleanNetwork (M.width t) n ×
       List (BooleanNetwork (M.width t) n)) :=
   …

   Mentions: OAI.ExactQuantumFactoring.BooleanNetwork

2. lemma OAI.ExactQuantumFactoring.NodeMachine.fieldRows_length line 27
3. lemma OAI.ExactQuantumFactoring.NodeMachine.fieldRows_values line 30
4. lemma OAI.ExactQuantumFactoring.NodeMachine.fieldRows_counts line 36
5. lemma OAI.ExactQuantumFactoring.NodeMachine.fieldRows_table_length line 46
6. def OAI.ExactQuantumFactoring.NodeMachine.retainedOrder line 56

   Source documentation

   The literal order network already available at any retained stage, before adding its reversible phase-flag wrapper.

   def retainedOrder (t : ℕ) (a m : BooleanNetwork (M.width t) n) : BooleanNetwork (M.width t) n :=
   …

   Mentions: OAI.ExactQuantumFactoring.BooleanNetwork

7. lemma OAI.ExactQuantumFactoring.NodeMachine.retainedOrder_exact line 59
8. lemma OAI.ExactQuantumFactoring.NodeMachine.retainedOrder_count line 76