OAI/Computability/QuantumFactoring/BooleanAlgebra.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ExactQuantumFactoring.BooleanNetwork.rewire line 12

    Source documentation

    Wire routing is free: it refers to values already physically present.

    def rewire {n m l : ℕ} (c : BooleanNetwork n m) (f : Fin l → Fin m) : BooleanNetwork n l :=
…

    Mentions: OAI.ExactQuantumFactoring.BooleanNetwork

  2. lemma OAI.ExactQuantumFactoring.BooleanNetwork.eval_rewire line 15
  3. lemma OAI.ExactQuantumFactoring.BooleanNetwork.count_rewire line 18
  4. def OAI.ExactQuantumFactoring.BooleanNetwork.bit line 21
  5. def OAI.ExactQuantumFactoring.BooleanNetwork.constant line 22
  6. def OAI.ExactQuantumFactoring.BooleanNetwork.bnot line 23
  7. def OAI.ExactQuantumFactoring.BooleanNetwork.band line 24
  8. def OAI.ExactQuantumFactoring.BooleanNetwork.bor line 26
  9. def OAI.ExactQuantumFactoring.BooleanNetwork.bxor line 27
  10. def OAI.ExactQuantumFactoring.BooleanNetwork.mux line 29
  11. def OAI.ExactQuantumFactoring.BooleanNetwork.majority line 31
  12. lemma OAI.ExactQuantumFactoring.BooleanNetwork.eval_bit line 34
  13. lemma OAI.ExactQuantumFactoring.BooleanNetwork.eval_constant line 37
  14. lemma OAI.ExactQuantumFactoring.BooleanNetwork.eval_bnot line 40
  15. lemma OAI.ExactQuantumFactoring.BooleanNetwork.eval_band line 43
  16. lemma OAI.ExactQuantumFactoring.BooleanNetwork.eval_bor line 48
  17. lemma OAI.ExactQuantumFactoring.BooleanNetwork.eval_bxor line 52
  18. lemma OAI.ExactQuantumFactoring.BooleanNetwork.eval_mux line 57
  19. lemma OAI.ExactQuantumFactoring.BooleanNetwork.eval_majority line 62
  20. lemma OAI.ExactQuantumFactoring.BooleanNetwork.count_bit line 67
  21. lemma OAI.ExactQuantumFactoring.BooleanNetwork.count_constant line 68
  22. lemma OAI.ExactQuantumFactoring.BooleanNetwork.count_bnot line 69
  23. lemma OAI.ExactQuantumFactoring.BooleanNetwork.count_band line 71
  24. lemma OAI.ExactQuantumFactoring.BooleanNetwork.count_bor line 73
  25. lemma OAI.ExactQuantumFactoring.BooleanNetwork.count_bxor line 75
  26. lemma OAI.ExactQuantumFactoring.BooleanNetwork.count_mux line 77
  27. lemma OAI.ExactQuantumFactoring.BooleanNetwork.count_majority line 79
  28. def OAI.ExactQuantumFactoring.BooleanNetwork.assign line 85

    Source documentation

    Logical assignment preserves the input values in the physical trace, but provides the standard overwritten-state interface to the next computation.

    def assign {n : ℕ} (i : Fin n) (v : BooleanNetwork n 1) : BooleanNetwork n n :=
…

    Mentions: OAI.ExactQuantumFactoring.BooleanNetwork

  29. lemma OAI.ExactQuantumFactoring.BooleanNetwork.eval_assign line 88
  30. lemma OAI.ExactQuantumFactoring.BooleanNetwork.count_assign line 97
  31. def OAI.ExactQuantumFactoring.BooleanNetwork.sequence line 101

    Source documentation

    Sequentially composed bounded logical updates compile by retained history.

    def sequence {n : ℕ} : List (BooleanNetwork n n) → BooleanNetwork n n
  | [] => select id
  | c :: cs => c.comp (sequence cs)

    Mentions: OAI.ExactQuantumFactoring.BooleanNetwork, OAI.ExactQuantumFactoring.BooleanNetwork.select

  32. lemma OAI.ExactQuantumFactoring.BooleanNetwork.eval_sequence line 105
  33. lemma OAI.ExactQuantumFactoring.BooleanNetwork.count_sequence line 111
  34. def OAI.ExactQuantumFactoring.BooleanNetwork.iterate line 117
  35. lemma OAI.ExactQuantumFactoring.BooleanNetwork.eval_iterate line 120
  36. lemma OAI.ExactQuantumFactoring.BooleanNetwork.count_iterate line 128