OAI/Computability/QuantumFactoring/TriangularKernel.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ExactQuantumFactoring.Triangular.phase_half line 15
2. lemma OAI.ExactQuantumFactoring.Triangular.phase_nat_half line 20
3. lemma OAI.ExactQuantumFactoring.Triangular.phase_product line 29
4. def OAI.ExactQuantumFactoring.Triangular.residuePhase line 51
5. lemma OAI.ExactQuantumFactoring.Triangular.residuePhase_correlation line 54
6. theorem OAI.ExactQuantumFactoring.Triangular.selected_kernel line 76

   Source documentation

   The full triangular coherent path expansion has exactly the manuscript's selected kernel, after the phase register is tested in its prepared state.

   theorem selected_kernel (a : ℕ) (x y : Bits (a+2)) :
       (∑ z : ZMod (2^(a+2)), star (residuePhase a z) *
         evolve (fun j v => (rowShift j v : ZMod (2^(a+2)))) x (residuePhase a)
           (a+2) le_rfl y z) =
         (Real.sqrt ((2:ℝ)^(a+2)) : ℂ)⁻¹ *
           phase ((inputNumber x:ℝ)*outputNumber y/(2:ℝ)^(a+2)) := by
   …

   Mentions: OAI.ExactQuantumFactoring.Triangular.Bits, OAI.ExactQuantumFactoring.Triangular.residuePhase, OAI.ExactQuantumFactoring.Triangular.evolve, OAI.ExactQuantumFactoring.Triangular.rowShift, OAI.ExactQuantumFactoring.Triangular.inputNumber, OAI.ExactQuantumFactoring.Triangular.outputNumber