OAI/Computability/QuantumFactoring/PrimalityPolynomial.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ExactQuantumFactoring.PreparationPolynomial.cyclicMulBound_poly line 16
2. lemma OAI.ExactQuantumFactoring.PreparationPolynomial.cyclicAddBound_poly line 24
3. lemma OAI.ExactQuantumFactoring.PreparationPolynomial.cyclicStepBound_poly line 31
4. lemma OAI.ExactQuantumFactoring.PreparationPolynomial.cyclicTestBound_poly line 36
5. lemma OAI.ExactQuantumFactoring.PreparationPolynomial.rootWidth_poly line 44
6. lemma OAI.ExactQuantumFactoring.PreparationPolynomial.perfectCheckBound_poly line 45
7. lemma OAI.ExactQuantumFactoring.PreparationPolynomial.aksBranchBound_poly line 51
8. lemma OAI.ExactQuantumFactoring.PreparationPolynomial.primalityBound_poly line 64
9. lemma OAI.ExactQuantumFactoring.PreparationPolynomial.primeBound_poly line 69
10. lemma OAI.ExactQuantumFactoring.PreparationPolynomial.guardBound_poly line 71
11. lemma OAI.ExactQuantumFactoring.PreparationPolynomial.quotientBound_poly line 74
12. lemma OAI.ExactQuantumFactoring.PreparationPolynomial.nodeStepBound_poly line 77