OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumPaddedLabelMeaning.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Every emitted local packet entry is the actual padded history word and its sampled coefficient, in the supplied support-list order.

  1. theorem OAI.ContinuumCoulomb.QuantumPaddedLabelProgram.labels_eq_zip line 17
  2. theorem OAI.ContinuumCoulomb.QuantumPaddedLabelProgram.entry_source line 27