OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumForkListPoints.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Literal numbering of the new active ports. A prefix sum of pair counts gives each center its contiguous block of fresh mediator indices.

  1. def OAI.ContinuumCoulomb.QuantumForkList.takeGroupsProgram line 12
  2. def OAI.ContinuumCoulomb.QuantumForkList.pairStartProgram line 24
  3. abbrev OAI.ContinuumCoulomb.QuantumForkList.PointInput line 27
  4. def OAI.ContinuumCoulomb.QuantumForkList.pointCode line 28
  5. def OAI.ContinuumCoulomb.QuantumForkList.freshPoint line 30
  6. def OAI.ContinuumCoulomb.QuantumForkList.freshPointProgram line 32
  7. abbrev OAI.ContinuumCoulomb.QuantumForkList.GroupInput line 45
  8. def OAI.ContinuumCoulomb.QuantumForkList.groupCode line 46
  9. def OAI.ContinuumCoulomb.QuantumForkList.nextGroupProgram line 48
  10. def OAI.ContinuumCoulomb.QuantumForkList.nextGroupsProgram line 65