OAI/Computability/QuantumFactoring/TriangularPreparation.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ExactQuantumFactoring.Triangular.phaseRegister line 15
  2. lemma OAI.ExactQuantumFactoring.Triangular.encode_phase line 24
  3. lemma OAI.ExactQuantumFactoring.Triangular.encode_outside_phase line 31
  4. lemma OAI.ExactQuantumFactoring.Triangular.encode_replace_phase line 47
  5. def OAI.ExactQuantumFactoring.Triangular.preparation line 59
  6. lemma OAI.ExactQuantumFactoring.Triangular.preparation_length line 62
  7. lemma OAI.ExactQuantumFactoring.Triangular.preparation_basis line 65
  8. def OAI.ExactQuantumFactoring.Triangular.transform line 85

    Source documentation

    Preparation, actual clean triangular gate program, inverse preparation. The success event is the all-zero phase and scratch register; it is not enforced.

    def transform (a : ℕ) : List (Instruction (width (a+2))) :=
…

    Mentions: OAI.ExactQuantumFactoring.Instruction, OAI.ExactQuantumFactoring.Triangular.width

  9. lemma OAI.ExactQuantumFactoring.Triangular.transform_length line 89
  10. theorem OAI.ExactQuantumFactoring.Triangular.transform_selected line 97

    Source documentation

    The exact selected matrix entry of an actual fixed-gate circuit.

    theorem transform_selected (a : ℕ) (x y : Bits (a+2)) :
    (programMatrix (transform a)).mulVec (basisVector (encode (a+2) (x,0)))
      (encode (a+2) (y,0)) =
      (Real.sqrt ((2:ℝ)^(a+2)) : ℂ)⁻¹ *
        OrderTrial.phase ((inputNumber x:ℝ)*outputNumber y/(2:ℝ)^(a+2)) := by
…

    Mentions: OAI.ExactQuantumFactoring.Triangular.Bits, OAI.ExactQuantumFactoring.programMatrix, OAI.ExactQuantumFactoring.Triangular.transform, OAI.ExactQuantumFactoring.basisVector, OAI.ExactQuantumFactoring.Triangular.encode, OAI.ExactQuantumFactoring.OrderTrial.phase, OAI.ExactQuantumFactoring.Triangular.inputNumber, OAI.ExactQuantumFactoring.Triangular.outputNumber