OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumGateUnitary.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Exact unitarity of the fixed verifier gates, needed for the circuit-to-Hamiltonian construction.

  1. theorem OAI.ContinuumCoulomb.qmaHadamard_gram line 13

    Distinct definitions of this name: OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumGates.lean:13 (same statement text; different proof or body). Qualify references as OAI.ContinuumCoulomb.qmaHadamard_gram@path.

  2. theorem OAI.ContinuumCoulomb.qmaPhaseT_gram line 21

    Distinct definitions of this name: OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumGates.lean:22 (same statement text; different proof or body). Qualify references as OAI.ContinuumCoulomb.qmaPhaseT_gram@path.

  3. theorem OAI.ContinuumCoulomb.sourceTensor_conjTranspose line 30
  4. theorem OAI.ContinuumCoulomb.sourceTensor_gram line 35
  5. theorem OAI.ContinuumCoulomb.qmaControlledNot_involutive line 42

    Distinct definitions of this name: OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumGates.lean:51 (different declaration text). Qualify references as OAI.ContinuumCoulomb.qmaControlledNot_involutive@path.

  6. theorem OAI.ContinuumCoulomb.qmaGateMatrix_gram line 57

    Distinct definitions of this name: OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumGates.lean:80 (different declaration text). Qualify references as OAI.ContinuumCoulomb.qmaGateMatrix_gram@path.

  7. theorem OAI.ContinuumCoulomb.qmaCircuitMatrix_gram line 88

    Distinct definitions of this name: OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumGates.lean:93 (same statement text; different proof or body). Qualify references as OAI.ContinuumCoulomb.qmaCircuitMatrix_gram@path.