OAI/Computability/QuantumFactoring/CircuitSemantics.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ExactQuantumFactoring.Instruction.Unused line 13
  2. def OAI.ExactQuantumFactoring.Instruction.splitBasis line 18

    Source documentation

    Reindex a full computational basis by the gate wires and all other wires. This is only a proof equivalence; it introduces no new gate in the model.

    noncomputable def Instruction.splitBasis {q : ℕ} (o : Instruction q) :
    Basis q ≃ Basis o.gate.arity × (o.Unused → Bool) := by
…

    Mentions: OAI.ExactQuantumFactoring.Instruction, OAI.ExactQuantumFactoring.Basis

  3. lemma OAI.ExactQuantumFactoring.tensor_unitary line 44
  4. lemma OAI.ExactQuantumFactoring.Instruction.matrix_eq_reindex line 54
  5. lemma OAI.ExactQuantumFactoring.Instruction.unitary line 74
  6. def OAI.ExactQuantumFactoring.programMatrix line 81

    Source documentation

    Matrix of executing a list of instructions, in chronological order.

    noncomputable def programMatrix {q : ℕ} (ops : List (Instruction q)) :
    Matrix (Basis q) (Basis q) ℂ :=
…

    Mentions: OAI.ExactQuantumFactoring.Instruction, OAI.ExactQuantumFactoring.Basis

  7. lemma OAI.ExactQuantumFactoring.programMatrix_fold line 85
  8. lemma OAI.ExactQuantumFactoring.programMatrix_unitary line 95
  9. lemma OAI.ExactQuantumFactoring.Circuit.apply_eq_matrix line 105
  10. def OAI.ExactQuantumFactoring.Gate.reverse line 120

    Source documentation

    Reversing a listed gate stays inside the same twenty gate names.

    def Gate.reverse (g : Gate) : Gate := {g with inverse := !g.inverse}

    Mentions: OAI.ExactQuantumFactoring.Gate

  11. lemma OAI.ExactQuantumFactoring.Gate.reverse_arity line 122
  12. lemma OAI.ExactQuantumFactoring.Gate.reverse_baseMatrix line 124
  13. lemma OAI.ExactQuantumFactoring.Gate.reverse_matrix line 128
  14. def OAI.ExactQuantumFactoring.Instruction.reverse line 145
  15. lemma OAI.ExactQuantumFactoring.Instruction.reverse_matrix line 148
  16. lemma OAI.ExactQuantumFactoring.programMatrix_append line 165
  17. lemma OAI.ExactQuantumFactoring.programMatrix_reverse line 171
  18. def OAI.ExactQuantumFactoring.Circuit.reverse line 182
  19. lemma OAI.ExactQuantumFactoring.unitary_finiteInner line 185
  20. lemma OAI.ExactQuantumFactoring.unitary_mass line 193
  21. lemma OAI.ExactQuantumFactoring.Circuit.mass line 199
  22. lemma OAI.ExactQuantumFactoring.Circuit.output_normalized line 204
  23. lemma OAI.ExactQuantumFactoring.Circuit.reverse_apply line 211