OAI/Computability/QuantumFactoring/TreeFinalResources.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ExactQuantumFactoring.PhysicalTree.amplifiedProgram_length line 18
2. lemma OAI.ExactQuantumFactoring.PhysicalTree.amplifiedOutput_count line 23
3. lemma OAI.ExactQuantumFactoring.PhysicalTree.paddedHistory_count line 27
4. lemma OAI.ExactQuantumFactoring.PhysicalTree.paddedOutputNet_count line 30
5. lemma OAI.ExactQuantumFactoring.PhysicalTree.quarterOutputNet_count line 34
6. lemma OAI.ExactQuantumFactoring.PhysicalTree.factoringProgram_length line 41
7. lemma OAI.ExactQuantumFactoring.PhysicalTree.readoutWidth_bound line 51
8. theorem OAI.ExactQuantumFactoring.PhysicalTree.factoringProgram_resources line 62

   Source documentation

   Concrete reduction of the remaining whole-program resource obligation to its literal preparation, accepted-event network, and root readout. These are counts of actual gates/wires, not an assumed big-O charge for arithmetic.

   theorem factoringProgram_resources (n : ℕ) (hn : 0<n) :
       (factoringProgram n hn).length≤3*(quarterProgram n).length+
         8*(quarterFlag n hn).net.count+16*quarterWidth n+
         4*(rootFlat n (2*n^2)).net.count+30*(n*n)+492 ∧
       readoutWidth n hn≤3*quarterWidth n+(quarterFlag n hn).net.count+
         (rootFlat n (2*n^2)).net.count+8*(n*n)+120 := by
   …

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