OAI/Computability/QuantumFactoring/TableOrderCircuit.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExactQuantumFactoring.BitArithmetic.tableFactor line 19

   Source documentation

   A zero/unused-row word is replaced by the harmless prime 2.

   def tableFactor {k n : ℕ} (label p : BooleanNetwork k n) : BooleanNetwork k n :=
   …

   Mentions: OAI.ExactQuantumFactoring.BooleanNetwork

2. lemma OAI.ExactQuantumFactoring.BitArithmetic.tableFactor_value line 22
3. lemma OAI.ExactQuantumFactoring.BitArithmetic.tableFactor_count line 36
4. def OAI.ExactQuantumFactoring.BitArithmetic.tableNets line 43
5. def OAI.ExactQuantumFactoring.BitArithmetic.tableValues line 46
6. lemma OAI.ExactQuantumFactoring.BitArithmetic.tableNets_values line 50
7. lemma OAI.ExactQuantumFactoring.BitArithmetic.tableNets_counts line 57
8. def OAI.ExactQuantumFactoring.BitArithmetic.orderFromList line 70

   Source documentation

   Start at the complete product of a known prime list and scan it once. This is sufficient whenever the group order divides that product.

   def orderFromList {k w : ℕ} (a m : BooleanNetwork k w) (qs : List (BooleanNetwork k w)) :
       BooleanNetwork k w :=
   …

   Mentions: OAI.ExactQuantumFactoring.BooleanNetwork

9. lemma OAI.ExactQuantumFactoring.BitArithmetic.orderFromList_unit line 74
10. lemma OAI.ExactQuantumFactoring.BitArithmetic.orderFromList_count line 89
11. lemma OAI.ExactQuantumFactoring.BitArithmetic.word_list_product_bound line 100

    Source documentation

    A uniform polynomial-width exact product bound.

    lemma word_list_product_bound {k w n : ℕ} (qs : List (BooleanNetwork k w)) (x : Basis k)
        (h : ∀ q∈qs,(bitsValue (q.eval x)).toNat≤2^n) :
        (qs.map (fun q=>(bitsValue (q.eval x)).toNat)).prod<2^(n*qs.length+1) := by
    …

    Mentions: OAI.ExactQuantumFactoring.BooleanNetwork, OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.bitsValue