OAI/MathematicalPhysics/ContinuumCoulomb/Reduction/SourceFinalGraph.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

The exact final graph indexed by the literal output vertex count. Changing only the proof of that count preserves every bond and weight.

  1. def OAI.ContinuumCoulomb.MediatorIteration.Bonds.castSites line 12
  2. theorem OAI.ContinuumCoulomb.MediatorIteration.Bonds.castSites_toList line 14
  3. theorem OAI.ContinuumCoulomb.MediatorIteration.Bonds.castSites_weight line 17
  4. theorem OAI.ContinuumCoulomb.MediatorIteration.Bonds.castSites_left line 20
  5. theorem OAI.ContinuumCoulomb.MediatorIteration.Bonds.castSites_right line 23
  6. theorem OAI.ContinuumCoulomb.MediatorIteration.Bonds.castSites_noLoops line 26
  7. theorem OAI.ContinuumCoulomb.MediatorIteration.Bonds.castSites_simple line 29
  8. abbrev OAI.ContinuumCoulomb.SourcePositiveProgram.graphEdgeCount line 37
  9. def OAI.ContinuumCoulomb.SourcePositiveProgram.graph line 42
  10. theorem OAI.ContinuumCoulomb.SourcePositiveProgram.graph_toList line 47
  11. theorem OAI.ContinuumCoulomb.SourcePositiveProgram.graph_weight line 53
  12. theorem OAI.ContinuumCoulomb.SourcePositiveProgram.graph_noLoops line 59
  13. theorem OAI.ContinuumCoulomb.SourcePositiveProgram.graph_simple line 63
  14. theorem OAI.ContinuumCoulomb.SourcePositiveProgram.hubbardGraph_exists line 67