OAI/Computability/QuantumFactoring/FactorVerifierBounds.lean
9 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.ExactQuantumFactoring.BitArithmetic.zeroWord_countline 13 - lemma
OAI.ExactQuantumFactoring.BitArithmetic.primeOrZero_countline 20 - lemma
OAI.ExactQuantumFactoring.BitArithmetic.paddedPair_countline 27 - lemma
OAI.ExactQuantumFactoring.BitArithmetic.unpadWord_countline 35 - lemma
OAI.ExactQuantumFactoring.BitArithmetic.productNet_countline 41 - abbrev
OAI.ExactQuantumFactoring.BitArithmetic.candidateProductBoundline 53 - lemma
OAI.ExactQuantumFactoring.BitArithmetic.candidateProduct_countline 56 - abbrev
OAI.ExactQuantumFactoring.BitArithmetic.factorVerifierBoundline 70 - lemma
OAI.ExactQuantumFactoring.BitArithmetic.factorVerifierOn_countline 75