OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumOrderedSupport.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Literal short support lists for the time-ordered history compiler. The list order, duplicate removal, and local-coordinate equivalence are explicit; no arbitrary finite-type enumeration enters the input algorithm.

  1. def OAI.ContinuumCoulomb.QuantumOrderedSupport.gateSites line 14
  2. theorem OAI.ContinuumCoulomb.QuantumOrderedSupport.gateSites_finset line 19
  3. theorem OAI.ContinuumCoulomb.QuantumOrderedSupport.gateSites_length line 23
  4. def OAI.ContinuumCoulomb.QuantumOrderedSupport.propagationSites line 26
  5. theorem OAI.ContinuumCoulomb.QuantumOrderedSupport.propagationSites_finset line 31
  6. theorem OAI.ContinuumCoulomb.QuantumOrderedSupport.propagationSites_length line 36
  7. def OAI.ContinuumCoulomb.QuantumOrderedSupport.distributedSites line 42
  8. theorem OAI.ContinuumCoulomb.QuantumOrderedSupport.distributedSites_finset line 53
  9. theorem OAI.ContinuumCoulomb.QuantumOrderedSupport.distributedSites_length line 64
  10. abbrev OAI.ContinuumCoulomb.QuantumOrderedSupport.Qubit line 74
  11. def OAI.ContinuumCoulomb.QuantumOrderedSupport.rawSites line 76
  12. theorem OAI.ContinuumCoulomb.QuantumOrderedSupport.rawSites_finset line 83
  13. theorem OAI.ContinuumCoulomb.QuantumOrderedSupport.rawSites_length line 93
  14. def OAI.ContinuumCoulomb.QuantumOrderedSupport.sites line 102
  15. theorem OAI.ContinuumCoulomb.QuantumOrderedSupport.sites_nodup line 106
  16. theorem OAI.ContinuumCoulomb.QuantumOrderedSupport.sites_finset line 110
  17. theorem OAI.ContinuumCoulomb.QuantumOrderedSupport.sites_length line 115
  18. def OAI.ContinuumCoulomb.QuantumOrderedSupport.supportEquiv line 120
  19. theorem OAI.ContinuumCoulomb.QuantumOrderedSupport.supportEquiv_apply line 128
  20. def OAI.ContinuumCoulomb.QuantumOrderedSupport.siteNumber line 132
  21. theorem OAI.ContinuumCoulomb.QuantumOrderedSupport.siteNumber_lt line 137
  22. theorem OAI.ContinuumCoulomb.QuantumOrderedSupport.siteNumber_injective line 142
  23. def OAI.ContinuumCoulomb.QuantumOrderedSupport.encodedSites line 158
  24. theorem OAI.ContinuumCoulomb.QuantumOrderedSupport.encodedSites_nodup line 162
  25. theorem OAI.ContinuumCoulomb.QuantumOrderedSupport.encodedSites_length line 166