OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumRawIncidence.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The literal four-spin exchange list preserves a uniform incidence bound. All bonds are counted, including bonds with zero weight.

  1. theorem OAI.ContinuumCoulomb.QuantumRawIncidence.degree_le_length line 16
  2. theorem OAI.ContinuumCoulomb.QuantumRawIncidence.degree_zero line 23
  3. theorem OAI.ContinuumCoulomb.QuantumRawIncidence.degree_flatten line 31
  4. def OAI.ContinuumCoulomb.QuantumRawIncidence.sites line 35
  5. theorem OAI.ContinuumCoulomb.QuantumRawIncidence.slot_div line 40
  6. theorem OAI.ContinuumCoulomb.QuantumRawIncidence.field_origin line 42
  7. theorem OAI.ContinuumCoulomb.QuantumRawIncidence.cross_origin line 52
  8. theorem OAI.ContinuumCoulomb.QuantumRawIncidence.packed_origin line 66
  9. theorem OAI.ContinuumCoulomb.QuantumRawIncidence.ofSites_subset line 84
  10. theorem OAI.ContinuumCoulomb.QuantumRawIncidence.term_degree line 97
  11. theorem OAI.ContinuumCoulomb.QuantumRawIncidence.penalty_degree line 115
  12. theorem OAI.ContinuumCoulomb.QuantumRawIncidence.raw_degree line 143
  13. theorem OAI.ContinuumCoulomb.QuantumRawIncidence.numbered_bound line 172