OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/SingleSpinSource.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

A literal, constant-size decision branch covers the original one-spin source. This prevents the many-electron construction from excluding it.

  1. theorem OAI.ContinuumCoulomb.source_one_vertex_edges line 14
  2. theorem OAI.ContinuumCoulomb.source_one_vertex_energy line 23
  3. def OAI.ContinuumCoulomb.SingleSpinSource.value line 37
  4. opaque OAI.ContinuumCoulomb.SingleSpinSource.program line 40
  5. theorem OAI.ContinuumCoulomb.SingleSpinSource.yes line 48
  6. theorem OAI.ContinuumCoulomb.SingleSpinSource.no line 56