OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumPaddedLabelTable.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The literal concatenation of fixed-width history packets is an exact enumeration of the actual padded history family. The local pattern order is allowed to depend on the support width; its explicit bijection is retained.

  1. theorem OAI.ContinuumCoulomb.QuantumPaddedLabelProgram.pattern_card line 15
  2. def OAI.ContinuumCoulomb.QuantumPaddedLabelProgram.packetPatterns line 20
  3. theorem OAI.ContinuumCoulomb.QuantumPaddedLabelProgram.packet_reindex line 24
  4. def OAI.ContinuumCoulomb.QuantumPaddedLabelProgram.sourceInput line 32
  5. def OAI.ContinuumCoulomb.QuantumPaddedLabelProgram.sourceEntries line 37
  6. def OAI.ContinuumCoulomb.QuantumPaddedLabelProgram.sourceTerms line 42
  7. def OAI.ContinuumCoulomb.QuantumPaddedLabelProgram.sourceWord line 50
  8. theorem OAI.ContinuumCoulomb.QuantumPaddedLabelProgram.sourceEntries_table line 53
  9. theorem OAI.ContinuumCoulomb.QuantumPaddedLabelProgram.sourceEntries_length line 94