OAI/Computability/QuantumFactoring/TreeReadoutResources.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ExactQuantumFactoring.PhysicalTree.flattenWords_count line 19
2. lemma OAI.ExactQuantumFactoring.PhysicalTree.rootFlat_count line 25
3. theorem OAI.ExactQuantumFactoring.PhysicalTree.factoringProgram_resources_reduced line 37

   Source documentation

   All readout overhead is now bounded by an explicit polynomial expression; the two remaining size estimates are preparation and same-history flagging.

   theorem factoringProgram_resources_reduced (n : ℕ) (hn : 0<n) :
       (factoringProgram n hn).length≤3*(quarterProgram n).length+
         8*(quarterFlag n hn).net.count+16*quarterWidth n+
         4*PhysicalNode.resultBound n+34*(n*n)+492 ∧
       readoutWidth n hn≤3*quarterWidth n+(quarterFlag n hn).net.count+
         PhysicalNode.resultBound n+9*(n*n)+120 := by
   …

   Mentions: OAI.ExactQuantumFactoring.PhysicalTree.factoringProgram, OAI.ExactQuantumFactoring.PhysicalTree.quarterProgram, OAI.ExactQuantumFactoring.PhysicalTree.quarterFlag, OAI.ExactQuantumFactoring.PhysicalTree.quarterWidth, OAI.ExactQuantumFactoring.PhysicalNode.resultBound, OAI.ExactQuantumFactoring.PhysicalTree.readoutWidth