OAI/Computability/QuantumFactoring/ArithmeticPredicates.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ExactQuantumFactoring.BitArithmetic.ult line 14
  2. lemma OAI.ExactQuantumFactoring.BitArithmetic.ult_correct line 18
  3. lemma OAI.ExactQuantumFactoring.BitArithmetic.ult_count line 27
  4. def OAI.ExactQuantumFactoring.BitArithmetic.wordLt line 35
  5. lemma OAI.ExactQuantumFactoring.BitArithmetic.wordLt_eval line 38
  6. lemma OAI.ExactQuantumFactoring.BitArithmetic.wordLt_count line 42
  7. def OAI.ExactQuantumFactoring.BitArithmetic.wordLe line 48
  8. lemma OAI.ExactQuantumFactoring.BitArithmetic.wordLe_eval line 51
  9. lemma OAI.ExactQuantumFactoring.BitArithmetic.wordLe_count line 58
  10. def OAI.ExactQuantumFactoring.BitArithmetic.wordEq line 64
  11. lemma OAI.ExactQuantumFactoring.BitArithmetic.wordEq_eval line 67
  12. lemma OAI.ExactQuantumFactoring.BitArithmetic.wordEq_count line 85
  13. def OAI.ExactQuantumFactoring.BitArithmetic.staticPowerStep line 92

    Source documentation

    Static natural exponent, with retained accumulator and no repeated construction of earlier expressions. This circuit has O(e w²) Boolean nodes.

    def staticPowerStep (w : ℕ) : BooleanNetwork (w+w) (w+w) :=
…

    Mentions: OAI.ExactQuantumFactoring.BooleanNetwork

  14. def OAI.ExactQuantumFactoring.BitArithmetic.staticPower line 95
  15. lemma OAI.ExactQuantumFactoring.BitArithmetic.staticPowerStep_eval line 99
  16. lemma OAI.ExactQuantumFactoring.BitArithmetic.staticPower_iterate line 107
  17. lemma OAI.ExactQuantumFactoring.BitArithmetic.staticPower_eval line 122
  18. lemma OAI.ExactQuantumFactoring.BitArithmetic.staticPower_count line 131