OAI/Computability/QuantumFactoring/MaskedPreparation.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ExactQuantumFactoring.rightProgram_state line 20
2. lemma OAI.ExactQuantumFactoring.encode_append_supported line 27
3. def OAI.ExactQuantumFactoring.maskGate line 35
4. lemma OAI.ExactQuantumFactoring.maskGate_state line 43
5. def OAI.ExactQuantumFactoring.maskedPrefix line 54
6. def OAI.ExactQuantumFactoring.selectedPrefix line 58
7. lemma OAI.ExactQuantumFactoring.maskedPrefix_length line 63
8. lemma OAI.ExactQuantumFactoring.maskedPrefix_state line 70

   Source documentation

   The mask is ordinary retained input data. This equation is valid before any measurement and for arbitrary coherent states in the target register.

   lemma maskedPrefix_state (n k : ℕ) (h : k ≤ n) (mask : Basis n) (ψ : State n) :
       (programMatrix (maskedPrefix n k h)).mulVec (encodeState (fun y => Fin.append mask y) ψ)=
         encodeState (fun y => Fin.append mask y) ((programMatrix (selectedPrefix mask k h)).mulVec ψ) := by
   …

   Mentions: OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.State, OAI.ExactQuantumFactoring.programMatrix, OAI.ExactQuantumFactoring.maskedPrefix, OAI.ExactQuantumFactoring.encodeState, OAI.ExactQuantumFactoring.selectedPrefix

9. def OAI.ExactQuantumFactoring.prefixMask line 80
10. lemma OAI.ExactQuantumFactoring.selectedPrefix_eq line 82
11. lemma OAI.ExactQuantumFactoring.maskedPrefix_zero line 99

    Source documentation

    Uniformly n gates suffice for EVERY runtime width b<=n. Unlike n fair bits, the upper n-b bits remain exactly zero, as required for the source list success bound on small cofactors.

    lemma maskedPrefix_zero (n b : ℕ) (hb : b ≤ n) :
        (programMatrix (maskedPrefix n n le_rfl)).mulVec
          (basisVector (Fin.append (prefixMask n b) (fun _ => false))) =
          encodeState (fun y => Fin.append (prefixMask n b) y)
            (fun y => if ∀ i : Fin n,b ≤ i.val→y i=false then (Real.sqrt 2:ℂ)⁻¹^b else 0) := by
    …

    Mentions: OAI.ExactQuantumFactoring.programMatrix, OAI.ExactQuantumFactoring.maskedPrefix, OAI.ExactQuantumFactoring.basisVector, OAI.ExactQuantumFactoring.prefixMask, OAI.ExactQuantumFactoring.encodeState