OAI/Computability/QuantumFactoring/PhysicalTreeQueue.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ExactQuantumFactoring.PhysicalTree.capacity line 19
  2. abbrev OAI.ExactQuantumFactoring.PhysicalTree.configWidth line 20
  3. def OAI.ExactQuantumFactoring.PhysicalTree.query line 22
  4. def OAI.ExactQuantumFactoring.PhysicalTree.nodeResult line 24
  5. def OAI.ExactQuantumFactoring.PhysicalTree.fields line 26
  6. def OAI.ExactQuantumFactoring.PhysicalTree.old line 29
  7. def OAI.ExactQuantumFactoring.PhysicalTree.localNode line 31
  8. def OAI.ExactQuantumFactoring.PhysicalTree.pushed line 33
  9. def OAI.ExactQuantumFactoring.PhysicalTree.update line 40

    Source documentation

    Literal fixed-capacity pending-node controller. The current modulus is removed and this very node's distinct p−1 children are prepended in sorted order. An empty queue is an idle tick, not a new root query.

    def update (n : ℕ) : BooleanNetwork (configWidth n+NodeKernel.width n) (configWidth n) :=
…

    Mentions: OAI.ExactQuantumFactoring.BooleanNetwork, OAI.ExactQuantumFactoring.PhysicalTree.configWidth, OAI.ExactQuantumFactoring.NodeKernel.width

  10. lemma OAI.ExactQuantumFactoring.PhysicalTree.query_encoding line 43
  11. lemma OAI.ExactQuantumFactoring.PhysicalTree.old_append line 47
  12. lemma OAI.ExactQuantumFactoring.PhysicalTree.localNode_append line 51
  13. lemma OAI.ExactQuantumFactoring.PhysicalTree.fields_eval line 56
  14. lemma OAI.ExactQuantumFactoring.PhysicalTree.pushed_eval line 70
  15. lemma OAI.ExactQuantumFactoring.PhysicalTree.update_eval line 79
  16. lemma OAI.ExactQuantumFactoring.PhysicalTree.update_nil line 91
  17. theorem OAI.ExactQuantumFactoring.PhysicalTree.update_passed line 105

    Source documentation

    Passed physical local computation produces EXACT canonical children in the physical outer queue. It does not use trueData to select or initialize a query.

    theorem update_passed {n : ℕ} (hn : 128 ≤ n) (a : Basis n) (as : List (Basis n))
    (hlen : (a::as).length ≤ capacity n) (ha : 2 ≤ (bitsValue a).toNat)
    (r : NodeKernel.Raw n) (hp : NodeKernel.passed a r) :
    ∃ kids : List (Basis n), SortedWords.numbers kids=AuxiliaryTree.children (bitsValue a).toNat ∧
      (update n).eval (Fin.append (stackEncoding (capacity n) n (a::as)) (NodeKernel.encoding a r))=
        stackEncoding (capacity n) n (kids++as) := by
…

    Mentions: OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.PhysicalTree.capacity, OAI.ExactQuantumFactoring.bitsValue, OAI.ExactQuantumFactoring.NodeKernel.Raw, OAI.ExactQuantumFactoring.NodeKernel.passed, OAI.ExactQuantumFactoring.AuxiliaryTree.children, OAI.ExactQuantumFactoring.PhysicalTree.update, OAI.ExactQuantumFactoring.NodeKernel.encoding