OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumOrdinalSpatial.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Replace the abstract default slots by the explicit ordinal choice on the encoded spin and interaction labels. The finite Hamiltonian is unchanged.

  1. def OAI.ContinuumCoulomb.QMACellSlots.transport line 14
  2. theorem OAI.ContinuumCoulomb.relabel_density line 24
  3. def OAI.ContinuumCoulomb.QMASpatialExchangeModel.withOrdinalSlots line 39
  4. theorem OAI.ContinuumCoulomb.QMASpatialExchangeModel.withOrdinalSlots_energy line 45
  5. theorem OAI.ContinuumCoulomb.QMASpatialExchangeModel.withOrdinalSlots_qubit_index line 48
  6. theorem OAI.ContinuumCoulomb.QMASpatialExchangeModel.withOrdinalSlots_term_index line 52