OAI/Computability/QuantumFactoring/NodeControlCircuit.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ExactQuantumFactoring.BitArithmetic.properOn line 20
  2. lemma OAI.ExactQuantumFactoring.BitArithmetic.properOn_value line 24
  3. abbrev OAI.ExactQuantumFactoring.BitArithmetic.NodeCircuit.width line 36
  4. def OAI.ExactQuantumFactoring.BitArithmetic.NodeCircuit.pending line 38
  5. def OAI.ExactQuantumFactoring.BitArithmetic.NodeCircuit.divisor line 39
  6. def OAI.ExactQuantumFactoring.BitArithmetic.NodeCircuit.top line 40
  7. def OAI.ExactQuantumFactoring.BitArithmetic.NodeCircuit.popped line 42
  8. def OAI.ExactQuantumFactoring.BitArithmetic.NodeCircuit.quotient line 44
  9. def OAI.ExactQuantumFactoring.BitArithmetic.NodeCircuit.isPrime line 46
  10. def OAI.ExactQuantumFactoring.BitArithmetic.NodeCircuit.isDone line 47
  11. def OAI.ExactQuantumFactoring.BitArithmetic.NodeCircuit.isProper line 48
  12. def OAI.ExactQuantumFactoring.BitArithmetic.NodeCircuit.split line 49
  13. def OAI.ExactQuantumFactoring.BitArithmetic.NodeCircuit.next line 52
  14. def OAI.ExactQuantumFactoring.BitArithmetic.NodeCircuit.emitted line 55
  15. def OAI.ExactQuantumFactoring.BitArithmetic.NodeCircuit.failed line 57
  16. def OAI.ExactQuantumFactoring.BitArithmetic.NodeCircuit.step line 60
  17. def OAI.ExactQuantumFactoring.BitArithmetic.NodeCircuit.pack line 63
  18. lemma OAI.ExactQuantumFactoring.BitArithmetic.NodeCircuit.pending_pack line 66
  19. lemma OAI.ExactQuantumFactoring.BitArithmetic.NodeCircuit.divisor_pack line 70
  20. lemma OAI.ExactQuantumFactoring.BitArithmetic.NodeCircuit.top_pack line 74
  21. lemma OAI.ExactQuantumFactoring.BitArithmetic.NodeCircuit.popped_pack line 79
  22. lemma OAI.ExactQuantumFactoring.BitArithmetic.NodeCircuit.quotient_pack line 83
  23. lemma OAI.ExactQuantumFactoring.BitArithmetic.NodeCircuit.split_pack line 89
  24. lemma OAI.ExactQuantumFactoring.BitArithmetic.NodeCircuit.isPrime_pack line 96
  25. lemma OAI.ExactQuantumFactoring.BitArithmetic.NodeCircuit.isProper_pack line 101
  26. lemma OAI.ExactQuantumFactoring.BitArithmetic.NodeCircuit.isDone_pack line 107
  27. lemma OAI.ExactQuantumFactoring.BitArithmetic.NodeCircuit.next_pack_cons line 115

    Source documentation

    Literal guarded stack update for one node of the recursive producer. The source primality test is the Boolean AKS circuit, and division is a full word division circuit. No semantic factorization operation is used here.

    lemma next_pack_cons {s w : ℕ} (hw : 128 ≤ w) (a d : Basis w) (xs : List (Basis w))
    (h : xs.length ≤ s) (ha : 2 ≤ (bitsValue a).toNat) :
    (next s w).eval (pack (a::xs) d)=
      if (bitsValue a).toNat.Prime then stackEncoding (s+1) w xs
      else if ProperDivisor (bitsValue a).toNat (bitsValue d).toNat then
        stackEncoding (s+1) w (d::(quotient s w).eval (pack (a::xs) d)::xs)
      else stackEncoding (s+1) w (a::xs) := by
…

    Mentions: OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.bitsValue, OAI.ExactQuantumFactoring.BitArithmetic.NodeCircuit.next, OAI.ExactQuantumFactoring.BitArithmetic.NodeCircuit.pack, OAI.ExactQuantumFactoring.BitArithmetic.stackEncoding, OAI.ExactQuantumFactoring.BitArithmetic.NodeCircuit.quotient

  28. lemma OAI.ExactQuantumFactoring.BitArithmetic.NodeCircuit.emitted_pack_cons line 130
  29. lemma OAI.ExactQuantumFactoring.BitArithmetic.NodeCircuit.failed_pack_cons line 140