OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumPaddedLabelProgram.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Fixed-arity local history packets: sparse numeric labels and sampled algebraic coefficients share exactly the same fixed Pauli-word order.

  1. abbrev OAI.ContinuumCoulomb.QuantumPaddedLabelProgram.Input line 17
  2. def OAI.ContinuumCoulomb.QuantumPaddedLabelProgram.inputCode line 18
  3. def OAI.ContinuumCoulomb.QuantumPaddedLabelProgram.labels line 21
  4. def OAI.ContinuumCoulomb.QuantumPaddedLabelProgram.entry line 25
  5. def OAI.ContinuumCoulomb.QuantumPaddedLabelProgram.packet line 28
  6. opaque OAI.ContinuumCoulomb.QuantumPaddedLabelProgram.precisionProgram line 31
  7. opaque OAI.ContinuumCoulomb.QuantumPaddedLabelProgram.indicesProgram line 32
  8. opaque OAI.ContinuumCoulomb.QuantumPaddedLabelProgram.matrixProgram line 34
  9. def OAI.ContinuumCoulomb.QuantumPaddedLabelProgram.labelsProgram line 37
  10. opaque OAI.ContinuumCoulomb.QuantumPaddedLabelProgram.entryProgram line 46
  11. def OAI.ContinuumCoulomb.QuantumPaddedLabelProgram.packetProgram line 52
  12. def OAI.ContinuumCoulomb.QuantumPaddedLabelProgram.uniformPacket line 60
  13. opaque OAI.ContinuumCoulomb.QuantumPaddedLabelProgram.uniformProgram line 68
  14. theorem OAI.ContinuumCoulomb.QuantumPaddedLabelProgram.uniformPacket_eq line 82
  15. theorem OAI.ContinuumCoulomb.QuantumPaddedLabelProgram.packet_length line 87
  16. theorem OAI.ContinuumCoulomb.QuantumPaddedLabelProgram.uniformPacket_length line 92
  17. def OAI.ContinuumCoulomb.QuantumPaddedLabelProgram.certificate line 97