OAI/MathematicalPhysics/ContinuumCoulomb/Programs/SourceBranchProgram.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Literal completion of a many-spin source map on the one-spin branch. The resulting reduction covers every valid source instance.

  1. def OAI.ContinuumCoulomb.SourceBranchProgram.value line 14
  2. opaque OAI.ContinuumCoulomb.SourceBranchProgram.program line 17
  3. theorem OAI.ContinuumCoulomb.SourceBranchProgram.positive_output_vertices line 25
  4. def OAI.ContinuumCoulomb.SourceBranchProgram.reduction line 30