OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumPolarizedThird.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Seven literal rational Pauli words for the real-preserving third-order gadget. The two possibly imaginary factors use the same mediator phase.

  1. def OAI.ContinuumCoulomb.QuantumPolarizedThird.word line 16
  2. def OAI.ContinuumCoulomb.QuantumPolarizedThird.weight line 24
  3. theorem OAI.ContinuumCoulomb.QuantumPolarizedThird.weight_cast line 28
  4. theorem OAI.ContinuumCoulomb.QuantumPolarizedThird.sum_eq line 32
  5. theorem OAI.ContinuumCoulomb.QuantumPolarizedThird.support line 50
  6. theorem OAI.ContinuumCoulomb.QuantumPolarizedThird.even line 79