OAI/Computability/QuantumFactoring/RootCircuit.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ExactQuantumFactoring.BitArithmetic.rootWidth line 16

    Source documentation

    Width large enough for every candidate's e-th power, e≤n.

    abbrev rootWidth (n : ℕ) := n*n+1
  2. def OAI.ExactQuantumFactoring.BitArithmetic.rootModulus line 18
  3. def OAI.ExactQuantumFactoring.BitArithmetic.rootGuess line 19
  4. def OAI.ExactQuantumFactoring.BitArithmetic.rootNext line 21
  5. def OAI.ExactQuantumFactoring.BitArithmetic.rootNew line 24
  6. def OAI.ExactQuantumFactoring.BitArithmetic.rootStep line 28
  7. def OAI.ExactQuantumFactoring.BitArithmetic.rootPrefix line 31
  8. lemma OAI.ExactQuantumFactoring.BitArithmetic.rootModulus_eval line 35
  9. lemma OAI.ExactQuantumFactoring.BitArithmetic.rootGuess_eval line 39
  10. lemma OAI.ExactQuantumFactoring.BitArithmetic.rootNext_word line 44
  11. lemma OAI.ExactQuantumFactoring.BitArithmetic.rootStep_pack line 49
  12. lemma OAI.ExactQuantumFactoring.BitArithmetic.rootNext_value line 54
  13. lemma OAI.ExactQuantumFactoring.BitArithmetic.candidatePower_lt line 65
  14. lemma OAI.ExactQuantumFactoring.BitArithmetic.rootNew_value line 74
  15. lemma OAI.ExactQuantumFactoring.BitArithmetic.rootPrefix_value line 84
  16. lemma OAI.ExactQuantumFactoring.BitArithmetic.rootNext_count line 112
  17. lemma OAI.ExactQuantumFactoring.BitArithmetic.rootStep_count line 117
  18. lemma OAI.ExactQuantumFactoring.BitArithmetic.rootPrefix_count line 127
  19. def OAI.ExactQuantumFactoring.BitArithmetic.boundedRootNet line 136
  20. lemma OAI.ExactQuantumFactoring.BitArithmetic.boundedRootNet_value line 140
  21. lemma OAI.ExactQuantumFactoring.BitArithmetic.boundedRootNet_count line 159