OAI/Computability/QuantumFactoring/SortingCircuit.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ExactQuantumFactoring.BitArithmetic.SortedWords.layout line 19
  2. def OAI.ExactQuantumFactoring.BitArithmetic.SortedWords.headNet line 23
  3. def OAI.ExactQuantumFactoring.BitArithmetic.SortedWords.tailNet line 24
  4. lemma OAI.ExactQuantumFactoring.BitArithmetic.SortedWords.headNet_eval line 25
  5. lemma OAI.ExactQuantumFactoring.BitArithmetic.SortedWords.tailNet_eval line 29
  6. def OAI.ExactQuantumFactoring.BitArithmetic.SortedWords.keepHead line 35

    Source documentation

    A recursive subnetwork is used ONCE, with its prefix wire retained.

    def keepHead {w r : ℕ} (c : BooleanNetwork (tensorWidth w r) (tensorWidth w r)) :
    BooleanNetwork (tensorWidth w (r+1)) (tensorWidth w (r+1)) :=
…

    Mentions: OAI.ExactQuantumFactoring.BooleanNetwork, OAI.ExactQuantumFactoring.tensorWidth

  7. lemma OAI.ExactQuantumFactoring.BitArithmetic.SortedWords.keepHead_eval line 38
  8. lemma OAI.ExactQuantumFactoring.BitArithmetic.SortedWords.keepHead_count line 42
  9. def OAI.ExactQuantumFactoring.BitArithmetic.SortedWords.compareStep line 46
  10. lemma OAI.ExactQuantumFactoring.BitArithmetic.SortedWords.compareStep_eval line 52
  11. lemma OAI.ExactQuantumFactoring.BitArithmetic.SortedWords.compareStep_count line 67
  12. def OAI.ExactQuantumFactoring.BitArithmetic.SortedWords.insertNet line 73
  13. def OAI.ExactQuantumFactoring.BitArithmetic.SortedWords.sortNet line 76
  14. lemma OAI.ExactQuantumFactoring.BitArithmetic.SortedWords.insertNet_eval line 80
  15. lemma OAI.ExactQuantumFactoring.BitArithmetic.SortedWords.sortNet_eval line 100
  16. lemma OAI.ExactQuantumFactoring.BitArithmetic.SortedWords.insertNet_count line 114
  17. theorem OAI.ExactQuantumFactoring.BitArithmetic.SortedWords.sortNet_count line 123

    Source documentation

    Quadratic number of word comparisons, each a polynomial Boolean network. No expanded sorting expression duplicates its recursively generated circuits.

    theorem sortNet_count (w r : ℕ) : (sortNet w r).net.count ≤ r*r*(498*w+114) := by
…

    Mentions: OAI.ExactQuantumFactoring.BitArithmetic.SortedWords.sortNet