OAI/Computability/QuantumFactoring/FactorVerifier.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ExactQuantumFactoring.BitArithmetic.rootWidth_ge line 16
  2. def OAI.ExactQuantumFactoring.BitArithmetic.primeWord line 22

    Source documentation

    The range check makes the AKS interface exact also for the invalid 0,1 entries occurring in arbitrary uniform guesses.

    def primeWord (n : ℕ) : BooleanNetwork n 1 :=
…

    Mentions: OAI.ExactQuantumFactoring.BooleanNetwork

  3. lemma OAI.ExactQuantumFactoring.BitArithmetic.primeWord_value line 26
  4. lemma OAI.ExactQuantumFactoring.BitArithmetic.primeWord_count line 44
  5. def OAI.ExactQuantumFactoring.BitArithmetic.zeroWord line 53
  6. lemma OAI.ExactQuantumFactoring.BitArithmetic.zeroWord_value line 56
  7. def OAI.ExactQuantumFactoring.BitArithmetic.primeOrZero line 61
  8. lemma OAI.ExactQuantumFactoring.BitArithmetic.primeOrZero_value line 64
  9. def OAI.ExactQuantumFactoring.BitArithmetic.paddedPair line 69
  10. lemma OAI.ExactQuantumFactoring.BitArithmetic.paddedPair_value line 72
  11. def OAI.ExactQuantumFactoring.BitArithmetic.unpadWord line 79
  12. lemma OAI.ExactQuantumFactoring.BitArithmetic.unpadWord_value line 82
  13. def OAI.ExactQuantumFactoring.BitArithmetic.productNet line 94

    Source documentation

    Multiplication is modulo the sufficiently wide product register; no repetition of earlier expression DAGs occurs in this linear fold.

    def productNet {k w : ℕ} : List (BooleanNetwork k w) → BooleanNetwork k w
  | [] => wordConstant 1
  | a::as => (a.pair (productNet as)).comp (mul w)

    Mentions: OAI.ExactQuantumFactoring.BooleanNetwork, OAI.ExactQuantumFactoring.BitArithmetic.wordConstant, OAI.ExactQuantumFactoring.BitArithmetic.mul

  14. lemma OAI.ExactQuantumFactoring.BitArithmetic.productNet_value line 98
  15. lemma OAI.ExactQuantumFactoring.BitArithmetic.productNet_nat line 104
  16. def OAI.ExactQuantumFactoring.BitArithmetic.candidateWords line 113
  17. def OAI.ExactQuantumFactoring.BitArithmetic.candidateProduct line 116
  18. lemma OAI.ExactQuantumFactoring.BitArithmetic.candidateProduct_value line 119
  19. def OAI.ExactQuantumFactoring.BitArithmetic.factorVerifierOn line 146
  20. lemma OAI.ExactQuantumFactoring.BitArithmetic.factorVerifierOn_correct line 154