OAI/MathematicalPhysics/ContinuumCoulomb/ManyBody/MediatorListCorrectness.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The concrete TM2 bond lists are exactly the enumerations of the finite spin matrices whose three-stage bottom-energy estimates were proved.

  1. abbrev OAI.ContinuumCoulomb.MediatorIteration.Bond line 12
  2. def OAI.ContinuumCoulomb.MediatorIteration.Bonds.toList line 14
  3. theorem OAI.ContinuumCoulomb.MediatorIteration.Bonds.toList_length line 17
  4. theorem OAI.ContinuumCoulomb.MediatorIteration.Bonds.toList_get line 20
  5. theorem OAI.ContinuumCoulomb.MediatorIteration.old_val line 27
  6. theorem OAI.ContinuumCoulomb.MediatorIteration.fresh_val line 29
  7. theorem OAI.ContinuumCoulomb.MediatorIteration.lift_toList line 34
  8. theorem OAI.ContinuumCoulomb.MediatorIteration.join_toList line 38
  9. theorem OAI.ContinuumCoulomb.MediatorIteration.central_toList_input line 52
  10. theorem OAI.ContinuumCoulomb.MediatorIteration.spokes_toList_input line 61