OAI/Computability/QuantumFactoring/NodeControlBounds.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ExactQuantumFactoring.BitArithmetic.properOn_count line 18
  2. def OAI.ExactQuantumFactoring.BitArithmetic.NodeCircuit.primeBound line 31
  3. def OAI.ExactQuantumFactoring.BitArithmetic.NodeCircuit.guardBound line 32
  4. def OAI.ExactQuantumFactoring.BitArithmetic.NodeCircuit.quotientBound line 33
  5. def OAI.ExactQuantumFactoring.BitArithmetic.NodeCircuit.splitBound line 34
  6. def OAI.ExactQuantumFactoring.BitArithmetic.NodeCircuit.nextBound line 35
  7. def OAI.ExactQuantumFactoring.BitArithmetic.NodeCircuit.stepBound line 37
  8. lemma OAI.ExactQuantumFactoring.BitArithmetic.NodeCircuit.pending_count line 39
  9. lemma OAI.ExactQuantumFactoring.BitArithmetic.NodeCircuit.top_count line 40
  10. lemma OAI.ExactQuantumFactoring.BitArithmetic.NodeCircuit.divisor_count line 41
  11. lemma OAI.ExactQuantumFactoring.BitArithmetic.NodeCircuit.popped_count line 42
  12. lemma OAI.ExactQuantumFactoring.BitArithmetic.NodeCircuit.quotient_count line 44
  13. lemma OAI.ExactQuantumFactoring.BitArithmetic.NodeCircuit.isPrime_count line 47
  14. lemma OAI.ExactQuantumFactoring.BitArithmetic.NodeCircuit.isDone_count line 49
  15. lemma OAI.ExactQuantumFactoring.BitArithmetic.NodeCircuit.isProper_count line 51
  16. lemma OAI.ExactQuantumFactoring.BitArithmetic.NodeCircuit.split_count line 54
  17. lemma OAI.ExactQuantumFactoring.BitArithmetic.NodeCircuit.next_count line 60
  18. lemma OAI.ExactQuantumFactoring.BitArithmetic.NodeCircuit.emitted_count line 69
  19. lemma OAI.ExactQuantumFactoring.BitArithmetic.NodeCircuit.failed_count line 73
  20. theorem OAI.ExactQuantumFactoring.BitArithmetic.NodeCircuit.step_count line 81

    Source documentation

    Explicit polynomial-size bound for the full guarded one-step controller.

    theorem step_count (s w : ℕ) : (step s w).net.count ≤ stepBound s w := by
…

    Mentions: OAI.ExactQuantumFactoring.BitArithmetic.NodeCircuit.step, OAI.ExactQuantumFactoring.BitArithmetic.NodeCircuit.stepBound