OAI/Computability/QuantumFactoring/CyclicPowerCircuit.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ExactQuantumFactoring.BitArithmetic.cyclicPowerWidth line 14
  2. def OAI.ExactQuantumFactoring.BitArithmetic.cyclicPack line 16
  3. def OAI.ExactQuantumFactoring.BitArithmetic.cyclicBase line 20
  4. def OAI.ExactQuantumFactoring.BitArithmetic.cyclicMod line 22
  5. def OAI.ExactQuantumFactoring.BitArithmetic.cyclicAcc line 24
  6. def OAI.ExactQuantumFactoring.BitArithmetic.cyclicBit line 26
  7. lemma OAI.ExactQuantumFactoring.BitArithmetic.cyclicBase_eval line 29
  8. lemma OAI.ExactQuantumFactoring.BitArithmetic.cyclicMod_eval line 33
  9. lemma OAI.ExactQuantumFactoring.BitArithmetic.cyclicAcc_eval line 37
  10. lemma OAI.ExactQuantumFactoring.BitArithmetic.cyclicBit_eval line 41
  11. def OAI.ExactQuantumFactoring.BitArithmetic.cyclicNew line 45
  12. def OAI.ExactQuantumFactoring.BitArithmetic.cyclicStep line 50
  13. lemma OAI.ExactQuantumFactoring.BitArithmetic.cyclicStep_pack line 54
  14. lemma OAI.ExactQuantumFactoring.BitArithmetic.cyclicNew_value line 63
  15. lemma OAI.ExactQuantumFactoring.BitArithmetic.cyclicNew_canonical line 82
  16. lemma OAI.ExactQuantumFactoring.BitArithmetic.cyclicMulBound_mono line 91
  17. abbrev OAI.ExactQuantumFactoring.BitArithmetic.cyclicStepBound line 97
  18. lemma OAI.ExactQuantumFactoring.BitArithmetic.cyclicNew_count line 100
  19. lemma OAI.ExactQuantumFactoring.BitArithmetic.cyclicStep_count line 114
  20. def OAI.ExactQuantumFactoring.BitArithmetic.cyclicPrefix line 118
  21. lemma OAI.ExactQuantumFactoring.BitArithmetic.cyclicPrefix_count line 123
  22. lemma OAI.ExactQuantumFactoring.BitArithmetic.cyclicPrefix_value line 133
  23. def OAI.ExactQuantumFactoring.BitArithmetic.cyclicPower line 156

    Source documentation

    n-bit repeated squaring in the coefficient array; no exponential polynomial or algebraic root is part of the computation.

    def cyclicPower (s w b : ℕ) [NeZero s] : BooleanNetwork ((s*w+w)+b) (s*w) :=
…

    Mentions: OAI.ExactQuantumFactoring.BooleanNetwork

  24. lemma OAI.ExactQuantumFactoring.BitArithmetic.cyclicPower_count line 160
  25. lemma OAI.ExactQuantumFactoring.BitArithmetic.cyclicPower_value line 168