OAI/Computability/QuantumFactoring/QueueCoverage.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExactQuantumFactoring.AuxiliaryTree.seen line 18

   Source documentation

   Chronological node heads, in reverse recording order. Zero denotes a dummy slot after the pending queue has become empty. Duplicate occurrences remain.

   def seen (xs : List ℕ) : ℕ→List ℕ
     | 0=>[]
     | t+1=>(run t xs).headD 0::seen xs t

   Mentions: OAI.ExactQuantumFactoring.AuxiliaryTree.run

2. lemma OAI.ExactQuantumFactoring.AuxiliaryTree.head_or_advance line 22
3. lemma OAI.ExactQuantumFactoring.AuxiliaryTree.children_head line 30
4. lemma OAI.ExactQuantumFactoring.AuxiliaryTree.seen_or_pending_step line 37

   Source documentation

   Everything pending before a step is either the recorded head or remains pending afterwards. This assertion does not search the mathematical tree.

   lemma seen_or_pending_step {xs : List ℕ} {t a : ℕ}
       (h : a∈seen xs t ∨ a∈run t xs) : a∈seen xs (t+1) ∨ a∈run (t+1) xs := by
   …

   Mentions: OAI.ExactQuantumFactoring.AuxiliaryTree.seen, OAI.ExactQuantumFactoring.AuxiliaryTree.run

5. lemma OAI.ExactQuantumFactoring.AuxiliaryTree.original_covered line 45
6. lemma OAI.ExactQuantumFactoring.AuxiliaryTree.children_covered line 53

   Source documentation

   Every required p−1 child of every already visited node is itself either visited or still on the actual occurrence queue.

   lemma children_covered (xs : List ℕ) (t : ℕ) {m a : ℕ}
       (hm : m∈seen xs t) (ha : a∈children m) : a∈seen xs t ∨ a∈run t xs := by
   …

   Mentions: OAI.ExactQuantumFactoring.AuxiliaryTree.seen, OAI.ExactQuantumFactoring.AuxiliaryTree.children, OAI.ExactQuantumFactoring.AuxiliaryTree.run

7. lemma OAI.ExactQuantumFactoring.AuxiliaryTree.completed_root line 63
8. lemma OAI.ExactQuantumFactoring.AuxiliaryTree.completed_children line 67
9. lemma OAI.ExactQuantumFactoring.AuxiliaryTree.seen_length line 72