OAI/Computability/QuantumFactoring/RetainedTreeFilter.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExactQuantumFactoring.NodeMachine.treePrefixFilter line 21
2. def OAI.ExactQuantumFactoring.NodeMachine.acceptedNet line 27
3. lemma OAI.ExactQuantumFactoring.PhysicalTree.treePrefixFilter_passed line 32
4. theorem OAI.ExactQuantumFactoring.PhysicalTree.acceptedNet_iff_passed line 62

   Source documentation

   A fully assembled same-history Boolean flag on the actual physical tree. Completeness of the factor table is derived from its literal verification; it is not a hypothesis of this flag specification.

   theorem acceptedNet_iff_passed {n N : ℕ} (hn : 128≤n) (hN : 2≤N) (hb : N<2^n)
       (h : NodeMachine.Trace n (2*n^2)) :
       ((machine n).acceptedNet (by omega) (2*n^2)).eval
         ((machine n).encoded (initialQueue n N) (2*n^2) h) 0=true ↔
         (machine n).passed (initialQueue n N) (2*n^2) h := by
   …

   Mentions: OAI.ExactQuantumFactoring.NodeMachine.Trace, OAI.ExactQuantumFactoring.PhysicalTree.machine, OAI.ExactQuantumFactoring.PhysicalTree.initialQueue

5. lemma OAI.ExactQuantumFactoring.PhysicalTree.acceptedNet_iff_accepted line 78