OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumOrderedLabelData.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Ordered sparse site/letter arrays. Every word carries the already proved support list; the bounded gadget operations inspect at most six letters, and retain the original order even for identity letters.

  1. abbrev OAI.ContinuumCoulomb.QuantumOrderedLabelData.Letter line 15
  2. def OAI.ContinuumCoulomb.QuantumOrderedLabelData.tag line 17
  3. def OAI.ContinuumCoulomb.QuantumOrderedLabelData.partition line 20
  4. def OAI.ContinuumCoulomb.QuantumOrderedLabelData.yCount line 27
  5. def OAI.ContinuumCoulomb.QuantumOrderedLabelData.axis line 29
  6. theorem OAI.ContinuumCoulomb.QuantumOrderedLabelData.tag_length line 31
  7. theorem OAI.ContinuumCoulomb.QuantumOrderedLabelData.tag_take line 34
  8. theorem OAI.ContinuumCoulomb.QuantumOrderedLabelData.tag_drop line 38
  9. theorem OAI.ContinuumCoulomb.QuantumOrderedLabelData.partition_tag line 42
  10. theorem OAI.ContinuumCoulomb.QuantumOrderedLabelData.yCount_tag line 72
  11. theorem OAI.ContinuumCoulomb.QuantumOrderedLabelData.tag_restrict line 96