OAI/Computability/QuantumFactoring/ChildQueueCorrect.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExactQuantumFactoring.BitArithmetic.ChildQueue.naturalKids line 18
2. lemma OAI.ExactQuantumFactoring.BitArithmetic.ChildQueue.naturalKids_cons line 21
3. lemma OAI.ExactQuantumFactoring.BitArithmetic.ChildQueue.number_injective line 26
4. lemma OAI.ExactQuantumFactoring.BitArithmetic.ChildQueue.kids_numbers line 30
5. lemma OAI.ExactQuantumFactoring.BitArithmetic.ChildQueue.naturalKids_correct line 52

   Source documentation

   No factorization oracle is used in the queue circuit: the child list obtained from the ACTUAL correct sorted prime fields is the source's exact ordered child list, with distinct primes within one node and occurrence multiplicity outside it.

   lemma naturalKids_correct {N n : ℕ} {xs : List ℕ} (hN : 2 ≤ N)
       (hx : CorrectEncoding N n xs) : naturalKids xs=AuxiliaryTree.children N := by
   …

   Mentions: OAI.ExactQuantumFactoring.CorrectEncoding, OAI.ExactQuantumFactoring.BitArithmetic.ChildQueue.naturalKids, OAI.ExactQuantumFactoring.AuxiliaryTree.children

6. theorem OAI.ExactQuantumFactoring.BitArithmetic.ChildQueue.kids_correct line 92