OAI/Computability/QuantumFactoring/ChildQueue.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ExactQuantumFactoring.BitArithmetic.ChildQueue.predBits line 20
  2. def OAI.ExactQuantumFactoring.BitArithmetic.ChildQueue.kids line 25

    Source documentation

    Children from the distinct prime fields, ignoring zero padding and 2. Repeated labels in DIFFERENT node records are not identified.

    def kids {w : ℕ} : List (Basis w) → List (Basis w)
  | [] => []
  | a::as => if 2<(bitsValue a).toNat ∧ a∉as then predBits a::kids as else kids as

    Mentions: OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.bitsValue, OAI.ExactQuantumFactoring.BitArithmetic.ChildQueue.predBits

  3. def OAI.ExactQuantumFactoring.BitArithmetic.ChildQueue.wordMember line 29
  4. lemma OAI.ExactQuantumFactoring.BitArithmetic.ChildQueue.wordMember_eval line 32
  5. def OAI.ExactQuantumFactoring.BitArithmetic.ChildQueue.source line 46
  6. def OAI.ExactQuantumFactoring.BitArithmetic.ChildQueue.queue line 47
  7. def OAI.ExactQuantumFactoring.BitArithmetic.ChildQueue.liftWord line 48
  8. def OAI.ExactQuantumFactoring.BitArithmetic.ChildQueue.active line 50
  9. def OAI.ExactQuantumFactoring.BitArithmetic.ChildQueue.pushOne line 53
  10. def OAI.ExactQuantumFactoring.BitArithmetic.ChildQueue.pushAll line 62

    Source documentation

    Tail before head: the recursive network occurs just ONCE in the syntax. All original factor fields remain read-only while the bounded queue is updated.

    def pushAll {k w : ℕ} (s : ℕ) : List (BooleanNetwork k w) → BooleanNetwork (k+s*w) (k+s*w)
  | [] => select id
  | a::as => (pushAll s as).comp (pushOne s a as)

    Mentions: OAI.ExactQuantumFactoring.BooleanNetwork, OAI.ExactQuantumFactoring.BitArithmetic.ChildQueue.pushOne

  11. lemma OAI.ExactQuantumFactoring.BitArithmetic.ChildQueue.source_eval line 66
  12. lemma OAI.ExactQuantumFactoring.BitArithmetic.ChildQueue.queue_eval line 70
  13. lemma OAI.ExactQuantumFactoring.BitArithmetic.ChildQueue.active_eval line 75
  14. lemma OAI.ExactQuantumFactoring.BitArithmetic.ChildQueue.pushOne_eval line 84
  15. lemma OAI.ExactQuantumFactoring.BitArithmetic.ChildQueue.pushAll_eval line 106
  16. lemma OAI.ExactQuantumFactoring.BitArithmetic.ChildQueue.predBits_value line 116