OAI/Computability/QuantumFactoring/SplitCandidate.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ExactQuantumFactoring.candidateDivisor line 14
  2. lemma OAI.ExactQuantumFactoring.halfOrderResidue_nat line 17
  3. lemma OAI.ExactQuantumFactoring.candidateDivisor_trueOrder line 23
  4. def OAI.ExactQuantumFactoring.BitArithmetic.halfWord line 31
  5. lemma OAI.ExactQuantumFactoring.BitArithmetic.div_word line 34
  6. lemma OAI.ExactQuantumFactoring.BitArithmetic.sub_word line 42
  7. lemma OAI.ExactQuantumFactoring.BitArithmetic.halfWord_value line 50
  8. def OAI.ExactQuantumFactoring.BitArithmetic.halfPower line 57

    Source documentation

    The repeated-squaring exponent is wired most-significant bit first.

    def halfPower {k w : ℕ} (a m d : BooleanNetwork k w) : BooleanNetwork k w :=
…

    Mentions: OAI.ExactQuantumFactoring.BooleanNetwork

  9. lemma OAI.ExactQuantumFactoring.BitArithmetic.halfPower_value line 60
  10. def OAI.ExactQuantumFactoring.BitArithmetic.shiftedHalfPower line 73
  11. lemma OAI.ExactQuantumFactoring.BitArithmetic.shiftedHalfPower_value line 77
  12. def OAI.ExactQuantumFactoring.BitArithmetic.splitRawOn line 100
  13. lemma OAI.ExactQuantumFactoring.BitArithmetic.splitRawOn_value line 103