OAI/MathematicalPhysics/ContinuumCoulomb/ManyBody/MediatorUnaryThird.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Actual third-stage unary coefficient and vertex metadata. Separate opaque arithmetic nodes prevent expansion of the finite program text.

  1. opaque OAI.ContinuumCoulomb.MediatorUnaryProgram.secondDeltaRaw line 11
  2. opaque OAI.ContinuumCoulomb.MediatorUnaryProgram.secondDelta line 14
  3. opaque OAI.ContinuumCoulomb.MediatorUnaryProgram.secondSpokesRaw line 17
  4. opaque OAI.ContinuumCoulomb.MediatorUnaryProgram.secondSpokes line 20
  5. opaque OAI.ContinuumCoulomb.MediatorUnaryProgram.thirdBase line 24
  6. opaque OAI.ContinuumCoulomb.MediatorUnaryProgram.thirdHead line 27
  7. opaque OAI.ContinuumCoulomb.MediatorUnaryProgram.weightThreeRaw line 31
  8. opaque OAI.ContinuumCoulomb.MediatorUnaryProgram.weightThree line 37
  9. opaque OAI.ContinuumCoulomb.MediatorUnaryProgram.sixR line 41
  10. opaque OAI.ContinuumCoulomb.MediatorUnaryProgram.thirdN line 43
  11. def OAI.ContinuumCoulomb.MediatorUnaryProgram.thirdEnv line 46
  12. opaque OAI.ContinuumCoulomb.MediatorUnaryProgram.thirdProgramRaw line 48
  13. opaque OAI.ContinuumCoulomb.MediatorUnaryProgram.thirdProgram line 51