OAI/Computability/QuantumFactoring/TriangularPaths.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ExactQuantumFactoring.Triangular.Bits line 12
2. def OAI.ExactQuantumFactoring.Triangular.hybrid line 14
3. def OAI.ExactQuantumFactoring.Triangular.TailEq line 17
4. instance OAI.ExactQuantumFactoring.Triangular.(instance at line 20) line 20
5. lemma OAI.ExactQuantumFactoring.Triangular.hybrid_update line 24
6. lemma OAI.ExactQuantumFactoring.Triangular.hybrid_of_tail line 33
7. lemma OAI.ExactQuantumFactoring.Triangular.tail_update line 41
8. def OAI.ExactQuantumFactoring.Triangular.pathShift line 62

   Source documentation

   Path translations for H on ascending physical wires followed by a classically controlled translation on a separate additive register.

   def pathShift {b : ℕ} (δ : Fin b → Bits b → A) (x y : Bits b) :
       (k : ℕ) → k ≤ b → A
     | 0, _ => 0
     | k+1, h => pathShift δ x y k (by omega) + δ ⟨k,by omega⟩ (hybrid x y (k+1))

   Mentions: OAI.ExactQuantumFactoring.Triangular.Bits, OAI.ExactQuantumFactoring.Triangular.hybrid

9. def OAI.ExactQuantumFactoring.Triangular.hEntry line 67
10. def OAI.ExactQuantumFactoring.Triangular.pathWeight line 70
11. lemma OAI.ExactQuantumFactoring.Triangular.pathShift_update line 74
12. lemma OAI.ExactQuantumFactoring.Triangular.pathWeight_update line 81
13. def OAI.ExactQuantumFactoring.Triangular.evolve line 92

    Source documentation

    Exact pointwise action of the H/conditional-forward-translation sequence. There is no projection or forced-success operation in this evolution.

    noncomputable def evolve {b : ℕ} (δ : Fin b → Bits b → A) (x : Bits b) (χ : A → ℂ) :
        (k : ℕ) → k ≤ b → Bits b → A → ℂ
      | 0, _, y, z => if y = x then χ z else 0
      | k+1, h, y, z =>
        (evolve δ x χ k (by omega) (Function.update y ⟨k,by omega⟩ false)
          (z-δ ⟨k,by omega⟩ y) +
         (if y ⟨k,by omega⟩ then (-1:ℂ) else 1) *
         evolve δ x χ k (by omega) (Function.update y ⟨k,by omega⟩ true)
          (z-δ ⟨k,by omega⟩ y)) / (Real.sqrt 2 : ℂ)
    
    /-- Every data wire has a single H and therefore exactly one compatible path
    for each input/output pair, even though the phase register is coherent. -/

    Mentions: OAI.ExactQuantumFactoring.Triangular.Bits

14. theorem OAI.ExactQuantumFactoring.Triangular.evolve_path line 104

    Source documentation

    Every data wire has a single H and therefore exactly one compatible path for each input/output pair, even though the phase register is coherent.

    theorem evolve_path {b : ℕ} (δ : Fin b → Bits b → A) (x y : Bits b) (χ : A → ℂ)
        (k : ℕ) (hk : k ≤ b) (z : A) :
        evolve δ x χ k hk y z =
          if TailEq k x y then pathWeight x y k hk * χ (z-pathShift δ x y k hk) else 0 := by
    …

    Mentions: OAI.ExactQuantumFactoring.Triangular.Bits, OAI.ExactQuantumFactoring.Triangular.evolve, OAI.ExactQuantumFactoring.Triangular.TailEq, OAI.ExactQuantumFactoring.Triangular.pathWeight, OAI.ExactQuantumFactoring.Triangular.pathShift

15. lemma OAI.ExactQuantumFactoring.Triangular.evolve_full line 127