OAI/Computability/QuantumFactoring/GcdCircuit.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Clocked Euclidean arithmetic, including zero operands. The clock is linear in bit width, and every step is an actual Boolean modular divider.

  1. def OAI.ExactQuantumFactoring.BitArithmetic.euclidRun line 17
  2. lemma OAI.ExactQuantumFactoring.BitArithmetic.euclidRun_zero line 21
  3. lemma OAI.ExactQuantumFactoring.BitArithmetic.euclidRun_terminal line 24
  4. def OAI.ExactQuantumFactoring.BitArithmetic.euclidStep line 49
  5. def OAI.ExactQuantumFactoring.BitArithmetic.euclidPrefix line 55
  6. def OAI.ExactQuantumFactoring.BitArithmetic.gcdNet line 59
  7. lemma OAI.ExactQuantumFactoring.BitArithmetic.euclidStep_semantics line 62
  8. lemma OAI.ExactQuantumFactoring.BitArithmetic.euclidPrefix_semantics line 80
  9. lemma OAI.ExactQuantumFactoring.BitArithmetic.gcdNet_value line 95
  10. lemma OAI.ExactQuantumFactoring.BitArithmetic.euclidStep_count line 105
  11. lemma OAI.ExactQuantumFactoring.BitArithmetic.euclidPrefix_count line 112
  12. lemma OAI.ExactQuantumFactoring.BitArithmetic.gcdNet_count line 122