OAI/MathematicalPhysics/ContinuumCoulomb/ManyBody/FiniteSourceBranch.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The decidable one-spin branch completed using arbitrary fixed YES and NO instances, so that no atomic spectral formula is required.

  1. def OAI.ContinuumCoulomb.FiniteSourceBranch.value line 13
  2. opaque OAI.ContinuumCoulomb.FiniteSourceBranch.program line 17
  3. def OAI.ContinuumCoulomb.FiniteSourceBranch.reduction line 30