OAI/Computability/QuantumFactoring/FactoringInputLayout.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ExactQuantumFactoring.natBasis_apply line 17
2. def OAI.ExactQuantumFactoring.shiftedInput line 22

   Source documentation

   The sole nondeterministic-preparation branch bit precedes the retained N; all remaining physical input coordinates are clean.

   def shiftedInput (q n N : ℕ) : Basis q :=
   …

   Mentions: OAI.ExactQuantumFactoring.Basis

3. lemma OAI.ExactQuantumFactoring.packed_shifted line 25
4. lemma OAI.ExactQuantumFactoring.PhysicalTree.quarterZero_input line 37
5. lemma OAI.ExactQuantumFactoring.PhysicalTree.quarterWidth_input line 49
6. lemma OAI.ExactQuantumFactoring.PhysicalTree.quarterZero_shifted line 53
7. lemma OAI.ExactQuantumFactoring.PhysicalTree.amplifiedZero_shifted line 70
8. lemma OAI.ExactQuantumFactoring.PhysicalTree.factoringZero_shifted line 74