OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumOrderedLabelPacking.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Conversion of the actual ordered sparse labels into the literal raw X/Z instructions, including the explicit finite relabeling of their energy.

  1. def OAI.ContinuumCoulomb.QuantumOrderedLabelTable.numberedSites line 16
  2. def OAI.ContinuumCoulomb.QuantumOrderedLabelTable.numberedWord line 19
  3. theorem OAI.ContinuumCoulomb.QuantumOrderedLabelTable.tag_numbered line 22
  4. theorem OAI.ContinuumCoulomb.QuantumOrderedLabelTable.packed_table line 28
  5. theorem OAI.ContinuumCoulomb.QuantumOrderedLabelTable.numbered_sites_length line 42
  6. theorem OAI.ContinuumCoulomb.QuantumOrderedLabelTable.numbered_sites_nodup line 47
  7. theorem OAI.ContinuumCoulomb.QuantumOrderedLabelTable.numbered_support line 52
  8. theorem OAI.ContinuumCoulomb.QuantumOrderedLabelTable.numbered_cover line 59
  9. theorem OAI.ContinuumCoulomb.QuantumOrderedLabelTable.numbered_private line 70
  10. theorem OAI.ContinuumCoulomb.QuantumOrderedLabelTable.numbered_energy line 83