OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumOrderedXZPipeline.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

One literal rational six-local to two-local X/Z family. The intermediate types retain the original term index and the bounded gadget-word index.

  1. abbrev OAI.ContinuumCoulomb.QuantumOrderedXZ.ThreeTerm line 14
  2. abbrev OAI.ContinuumCoulomb.QuantumOrderedXZ.ThreeQubit line 15
  3. abbrev OAI.ContinuumCoulomb.QuantumOrderedXZ.TwoTerm line 16
  4. abbrev OAI.ContinuumCoulomb.QuantumOrderedXZ.TwoQubit line 17
  5. abbrev OAI.ContinuumCoulomb.QuantumOrderedXZ.XZThreeTerm line 18
  6. abbrev OAI.ContinuumCoulomb.QuantumOrderedXZ.XZThreeQubit line 19
  7. abbrev OAI.ContinuumCoulomb.QuantumOrderedXZ.OutputTerm line 20
  8. abbrev OAI.ContinuumCoulomb.QuantumOrderedXZ.OutputQubit line 21
  9. def OAI.ContinuumCoulomb.QuantumOrderedXZ.threeWord line 25
  10. def OAI.ContinuumCoulomb.QuantumOrderedXZ.threeSites line 28
  11. def OAI.ContinuumCoulomb.QuantumOrderedXZ.threeCoefficient line 31
  12. def OAI.ContinuumCoulomb.QuantumOrderedXZ.twoWord line 34
  13. def OAI.ContinuumCoulomb.QuantumOrderedXZ.twoSites line 38
  14. def OAI.ContinuumCoulomb.QuantumOrderedXZ.twoCoefficient line 42
  15. def OAI.ContinuumCoulomb.QuantumOrderedXZ.xzThreeWord line 45
  16. def OAI.ContinuumCoulomb.QuantumOrderedXZ.xzThreeSites line 49
  17. def OAI.ContinuumCoulomb.QuantumOrderedXZ.xzThreeCoefficient line 53
  18. def OAI.ContinuumCoulomb.QuantumOrderedXZ.word line 56
  19. def OAI.ContinuumCoulomb.QuantumOrderedXZ.sites line 60
  20. def OAI.ContinuumCoulomb.QuantumOrderedXZ.coefficient line 64
  21. theorem OAI.ContinuumCoulomb.QuantumOrderedXZ.threeSites_nodup line 68
  22. theorem OAI.ContinuumCoulomb.QuantumOrderedXZ.threeSites_length line 72
  23. theorem OAI.ContinuumCoulomb.QuantumOrderedXZ.threeSites_cover line 75
  24. theorem OAI.ContinuumCoulomb.QuantumOrderedXZ.three_even line 79
  25. theorem OAI.ContinuumCoulomb.QuantumOrderedXZ.twoSites_nodup line 86
  26. theorem OAI.ContinuumCoulomb.QuantumOrderedXZ.twoSites_length line 92
  27. theorem OAI.ContinuumCoulomb.QuantumOrderedXZ.twoSites_cover line 96
  28. theorem OAI.ContinuumCoulomb.QuantumOrderedXZ.two_even line 100
  29. theorem OAI.ContinuumCoulomb.QuantumOrderedXZ.xzThreeSites_nodup line 108
  30. theorem OAI.ContinuumCoulomb.QuantumOrderedXZ.xzThreeSites_length line 113
  31. theorem OAI.ContinuumCoulomb.QuantumOrderedXZ.xzThreeSites_cover line 117
  32. theorem OAI.ContinuumCoulomb.QuantumOrderedXZ.xzThree_noY line 125
  33. theorem OAI.ContinuumCoulomb.QuantumOrderedXZ.sites_nodup line 132
  34. theorem OAI.ContinuumCoulomb.QuantumOrderedXZ.sites_length line 138
  35. theorem OAI.ContinuumCoulomb.QuantumOrderedXZ.sites_cover line 142
  36. theorem OAI.ContinuumCoulomb.QuantumOrderedXZ.noY line 149
  37. theorem OAI.ContinuumCoulomb.QuantumOrderedXZ.support line 155
  38. theorem OAI.ContinuumCoulomb.QuantumOrderedXZ.term_count line 162
  39. theorem OAI.ContinuumCoulomb.QuantumOrderedXZ.qubit_count line 167