OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumOrderedRawPacking.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Raw scalar/field/pair instructions read directly from the ordered site-label list. Only two entries are inspected at the final X/Z stage.

  1. abbrev OAI.ContinuumCoulomb.QuantumOrderedRawPacking.Letter line 11
  2. abbrev OAI.ContinuumCoulomb.QuantumOrderedRawPacking.Input line 12
  3. def OAI.ContinuumCoulomb.QuantumOrderedRawPacking.scalar line 14
  4. def OAI.ContinuumCoulomb.QuantumOrderedRawPacking.field line 17
  5. def OAI.ContinuumCoulomb.QuantumOrderedRawPacking.pair line 21
  6. def OAI.ContinuumCoulomb.QuantumOrderedRawPacking.value line 24
  7. theorem OAI.ContinuumCoulomb.QuantumOrderedRawPacking.axis_zero line 32
  8. theorem OAI.ContinuumCoulomb.QuantumOrderedRawPacking.field_pack line 36
  9. theorem OAI.ContinuumCoulomb.QuantumOrderedRawPacking.value_pack line 44