OAI/Computability/QuantumFactoring/ModularPower.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ExactQuantumFactoring.BitArithmetic.powerWidth line 14
  2. def OAI.ExactQuantumFactoring.BitArithmetic.powerPack line 16
  3. def OAI.ExactQuantumFactoring.BitArithmetic.powerBase line 19
  4. def OAI.ExactQuantumFactoring.BitArithmetic.powerModulus line 21
  5. def OAI.ExactQuantumFactoring.BitArithmetic.powerAcc line 23
  6. def OAI.ExactQuantumFactoring.BitArithmetic.powerBit line 25
  7. lemma OAI.ExactQuantumFactoring.BitArithmetic.powerBase_eval line 28
  8. lemma OAI.ExactQuantumFactoring.BitArithmetic.powerModulus_eval line 32
  9. lemma OAI.ExactQuantumFactoring.BitArithmetic.powerAcc_eval line 37
  10. lemma OAI.ExactQuantumFactoring.BitArithmetic.powerBit_eval line 41
  11. def OAI.ExactQuantumFactoring.BitArithmetic.powerNew line 45
  12. def OAI.ExactQuantumFactoring.BitArithmetic.powerStep line 49
  13. lemma OAI.ExactQuantumFactoring.BitArithmetic.powerNew_count line 53
  14. lemma OAI.ExactQuantumFactoring.BitArithmetic.powerStep_count line 65
  15. lemma OAI.ExactQuantumFactoring.BitArithmetic.powerStep_pack line 71
  16. lemma OAI.ExactQuantumFactoring.BitArithmetic.powerNew_value line 79
  17. def OAI.ExactQuantumFactoring.BitArithmetic.horner line 95

    Source documentation

    Horner value processes the actual physical data bits from low wire to high wire, matching the reversed input convention of the triangular transform.

    def horner {b : ℕ} (e : Basis b) : (k : ℕ) → k ≤ b → ℕ
  | 0, _ => 0
  | k+1, h => 2*horner e k (by omega) + (e ⟨k,by omega⟩).toNat

    Mentions: OAI.ExactQuantumFactoring.Basis

  18. def OAI.ExactQuantumFactoring.BitArithmetic.powerPrefix line 99
  19. lemma OAI.ExactQuantumFactoring.BitArithmetic.powerPrefix_count line 103
  20. lemma OAI.ExactQuantumFactoring.BitArithmetic.horner_pow_step line 113
  21. lemma OAI.ExactQuantumFactoring.BitArithmetic.powerPrefix_value line 124
  22. def OAI.ExactQuantumFactoring.BitArithmetic.modularPower line 147

    Source documentation

    The complete bounded binary-power network. Inputs remain available for copying; the result is a separate output word.

    def modularPower (w b : ℕ) : BooleanNetwork ((w+w)+b) w :=
…

    Mentions: OAI.ExactQuantumFactoring.BooleanNetwork

  23. lemma OAI.ExactQuantumFactoring.BitArithmetic.modularPower_count line 151
  24. lemma OAI.ExactQuantumFactoring.BitArithmetic.modularPower_value line 158