OAI/Computability/QuantumFactoring/SuppliedDivisorCircuit.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ExactQuantumFactoring.Primality.rootSearch_lt line 17
  2. lemma OAI.ExactQuantumFactoring.Primality.boundedRoot_lt line 29
  3. def OAI.ExactQuantumFactoring.BitArithmetic.firstProperNet line 36
  4. lemma OAI.ExactQuantumFactoring.BitArithmetic.firstProperNet_value line 41
  5. def OAI.ExactQuantumFactoring.BitArithmetic.evenOn line 52
  6. lemma OAI.ExactQuantumFactoring.BitArithmetic.evenOn_value line 54
  7. def OAI.ExactQuantumFactoring.BitArithmetic.candidateOn line 60
  8. lemma OAI.ExactQuantumFactoring.BitArithmetic.candidateOn_value line 62
  9. def OAI.ExactQuantumFactoring.BitArithmetic.rootOn line 75
  10. lemma OAI.ExactQuantumFactoring.BitArithmetic.rootOn_value line 78
  11. def OAI.ExactQuantumFactoring.BitArithmetic.rootsOn line 87
  12. lemma OAI.ExactQuantumFactoring.BitArithmetic.rootsOn_value line 89
  13. def OAI.ExactQuantumFactoring.BitArithmetic.ordersOn line 97
  14. lemma OAI.ExactQuantumFactoring.BitArithmetic.ordersOn_value line 100
  15. def OAI.ExactQuantumFactoring.BitArithmetic.suppliedOn line 111
  16. theorem OAI.ExactQuantumFactoring.BitArithmetic.suppliedOn_value line 118

    Source documentation

    The actual even/root/order implementation. No factorization information is used in this decoder, and all loops are fixed by n and the number of slots.

    theorem suppliedOn_value {k n : ℕ} (hn : 0<n) (m : BooleanNetwork k (n+1))
    (ars : List (BooleanNetwork k (n+1) × BooleanNetwork k (n+1))) (x : Basis k)
    (hm : 2≤(bitsValue (m.eval x)).toNat) (hb : (bitsValue (m.eval x)).toNat<2^n) :
    (bitsValue ((suppliedOn n m ars).eval x)).toNat=suppliedDivisor (bitsValue (m.eval x)).toNat n
      (ars.map (fun ar => ((bitsValue (ar.1.eval x)).toNat,(bitsValue (ar.2.eval x)).toNat))) := by
…

    Mentions: OAI.ExactQuantumFactoring.BooleanNetwork, OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.bitsValue, OAI.ExactQuantumFactoring.BitArithmetic.suppliedOn, OAI.ExactQuantumFactoring.suppliedDivisor