OAI/Computability/QuantumFactoring/PhysicalOrderSlots.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ExactQuantumFactoring.OrderSlots.ordinaryWidth line 15
  2. abbrev OAI.ExactQuantumFactoring.OrderSlots.coinWidth line 16
  3. abbrev OAI.ExactQuantumFactoring.OrderSlots.width line 17
  4. def OAI.ExactQuantumFactoring.OrderSlots.ordinaryLayout line 19
  5. def OAI.ExactQuantumFactoring.OrderSlots.layout line 22
  6. def OAI.ExactQuantumFactoring.OrderSlots.program line 26
  7. def OAI.ExactQuantumFactoring.OrderSlots.zero line 30
  8. lemma OAI.ExactQuantumFactoring.OrderSlots.ordinary_entry line 33
  9. lemma OAI.ExactQuantumFactoring.OrderSlots.program_entry line 45

    Source documentation

    The completed order slot is a literal finite gate program on fresh qubits. Neither the true order nor retrospective factor data occur in its preparation.

    lemma program_entry (n : ℕ) (a m : Basis n) (r : Result n) :
    (programMatrix (program n)).mulVec (basisVector (layout n (zero a m))) (layout n r)=fresh n a m r := by
…

    Mentions: OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.OrderSlots.Result, OAI.ExactQuantumFactoring.programMatrix, OAI.ExactQuantumFactoring.OrderSlots.program, OAI.ExactQuantumFactoring.basisVector, OAI.ExactQuantumFactoring.OrderSlots.layout, OAI.ExactQuantumFactoring.OrderSlots.zero, OAI.ExactQuantumFactoring.OrderSlots.fresh

  10. lemma OAI.ExactQuantumFactoring.OrderSlots.program_state line 56
  11. lemma OAI.ExactQuantumFactoring.OrderSlots.program_mass line 63
  12. lemma OAI.ExactQuantumFactoring.OrderSlots.program_passed_mass line 72
  13. lemma OAI.ExactQuantumFactoring.OrderSlots.program_length line 78