OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumFourEncoding.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The two rational singlet columns spanning the four-spin encoded qubit.

  1. def OAI.ContinuumCoulomb.qmaFourRaw0 line 12
  2. def OAI.ContinuumCoulomb.qmaFourRaw1 line 13
  3. def OAI.ContinuumCoulomb.qmaFourRawEncoding line 15
  4. theorem OAI.ContinuumCoulomb.qmaFourRawEncoding_gram line 18
  5. theorem OAI.ContinuumCoulomb.qmaFourExchangeRational_mulVec line 25
  6. def OAI.ContinuumCoulomb.qmaFourRawLogical line 32
  7. theorem OAI.ContinuumCoulomb.qmaFourRawEncoding_action01 line 37
  8. theorem OAI.ContinuumCoulomb.qmaFourRawEncoding_action02 line 47
  9. theorem OAI.ContinuumCoulomb.qmaFourRawEncoding_action03 line 57
  10. theorem OAI.ContinuumCoulomb.qmaFourRawEncoding_action12 line 67
  11. theorem OAI.ContinuumCoulomb.qmaFourRawEncoding_action13 line 77
  12. theorem OAI.ContinuumCoulomb.qmaFourRawEncoding_action23 line 87
  13. theorem OAI.ContinuumCoulomb.qmaFourRawEncoding_action line 97