OAI/Computability/QuantumFactoring/AKSBounds.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ExactQuantumFactoring.BitArithmetic.aksBranchBound line 13
2. lemma OAI.ExactQuantumFactoring.BitArithmetic.aksBranch_count line 17
3. lemma OAI.ExactQuantumFactoring.BitArithmetic.aksBranchBound_mono line 29
4. lemma OAI.ExactQuantumFactoring.BitArithmetic.aksStaticBranch_count line 35
5. abbrev OAI.ExactQuantumFactoring.BitArithmetic.primalityBound line 48
6. theorem OAI.ExactQuantumFactoring.BitArithmetic.primalityNet_count line 53

   Source documentation

   Explicit polynomial size for the full exact primality network.

   theorem primalityNet_count (n : ℕ) : (primalityNet n).net.count ≤ primalityBound n := by
   …

   Mentions: OAI.ExactQuantumFactoring.BitArithmetic.primalityNet, OAI.ExactQuantumFactoring.BitArithmetic.primalityBound