OAI/MathematicalPhysics/ContinuumCoulomb/Programs/MediatorListProgram.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

Actual TM2 programs which emit the central and spoke bond lists of one simultaneous mediator stage. The index arithmetic follows the same n + 2e + spin vertex enumeration as the proved finite-spin construction.

  1. abbrev OAI.ContinuumCoulomb.MediatorListProgram.Bond line 13
  2. def OAI.ContinuumCoulomb.MediatorListProgram.bondCode line 15
  3. def OAI.ContinuumCoulomb.MediatorListProgram.zeroBond line 17
  4. abbrev OAI.ContinuumCoulomb.MediatorListProgram.Env line 19
  5. def OAI.ContinuumCoulomb.MediatorListProgram.envCode line 21
  6. abbrev OAI.ContinuumCoulomb.MediatorListProgram.IndexedBond line 23
  7. def OAI.ContinuumCoulomb.MediatorListProgram.indexedCode line 25
  8. def OAI.ContinuumCoulomb.MediatorListProgram.environment line 27
  9. def OAI.ContinuumCoulomb.MediatorListProgram.rProgram line 29
  10. def OAI.ContinuumCoulomb.MediatorListProgram.wProgram line 32
  11. def OAI.ContinuumCoulomb.MediatorListProgram.gProgram line 35
  12. def OAI.ContinuumCoulomb.MediatorListProgram.nProgram line 38
  13. def OAI.ContinuumCoulomb.MediatorListProgram.indexProgram line 41
  14. def OAI.ContinuumCoulomb.MediatorListProgram.bondProgram line 44
  15. def OAI.ContinuumCoulomb.MediatorListProgram.leftProgram line 47
  16. def OAI.ContinuumCoulomb.MediatorListProgram.rightProgram line 50
  17. def OAI.ContinuumCoulomb.MediatorListProgram.weightProgram line 53
  18. def OAI.ContinuumCoulomb.MediatorListProgram.parametersProgram line 56
  19. def OAI.ContinuumCoulomb.MediatorListProgram.amplitudeProgram line 60
  20. def OAI.ContinuumCoulomb.MediatorListProgram.halfProgram line 64
  21. def OAI.ContinuumCoulomb.MediatorListProgram.evenProgram line 67
  22. def OAI.ContinuumCoulomb.MediatorListProgram.negativeProgram line 71
  23. def OAI.ContinuumCoulomb.MediatorListProgram.spokeLeftProgram line 78
  24. def OAI.ContinuumCoulomb.MediatorListProgram.vertexBaseProgram line 82
  25. def OAI.ContinuumCoulomb.MediatorListProgram.spokeRightProgram line 87
  26. def OAI.ContinuumCoulomb.MediatorListProgram.spoke line 96
  27. def OAI.ContinuumCoulomb.MediatorListProgram.spokeProgram line 102
  28. abbrev OAI.ContinuumCoulomb.MediatorListProgram.Input line 105
  29. def OAI.ContinuumCoulomb.MediatorListProgram.inputCode line 107
  30. abbrev OAI.ContinuumCoulomb.MediatorListProgram.LoopInput line 109
  31. def OAI.ContinuumCoulomb.MediatorListProgram.loopCode line 111
  32. def OAI.ContinuumCoulomb.MediatorListProgram.loopIndex line 113
  33. def OAI.ContinuumCoulomb.MediatorListProgram.loopInput line 115
  34. def OAI.ContinuumCoulomb.MediatorListProgram.loopEnvironment line 117
  35. def OAI.ContinuumCoulomb.MediatorListProgram.loopEdges line 120
  36. def OAI.ContinuumCoulomb.MediatorListProgram.loopBond line 123
  37. def OAI.ContinuumCoulomb.MediatorListProgram.loopSpoke line 129
  38. def OAI.ContinuumCoulomb.MediatorListProgram.spokes line 133
  39. def OAI.ContinuumCoulomb.MediatorListProgram.spokesProgram line 136
  40. def OAI.ContinuumCoulomb.MediatorListProgram.centralBase line 144
  41. def OAI.ContinuumCoulomb.MediatorListProgram.centralWeight line 152
  42. def OAI.ContinuumCoulomb.MediatorListProgram.central line 167
  43. def OAI.ContinuumCoulomb.MediatorListProgram.centralProgram line 171
  44. def OAI.ContinuumCoulomb.MediatorListProgram.stageProgram line 183
  45. def OAI.ContinuumCoulomb.MediatorListProgram.encodedBondTuple line 187
  46. def OAI.ContinuumCoulomb.MediatorListProgram.encodedBondLeft line 193
  47. def OAI.ContinuumCoulomb.MediatorListProgram.encodedBondRest line 197
  48. def OAI.ContinuumCoulomb.MediatorListProgram.encodedBondRight line 203
  49. def OAI.ContinuumCoulomb.MediatorListProgram.encodedBondWeight line 207
  50. def OAI.ContinuumCoulomb.MediatorListProgram.encodedBond line 211
  51. def OAI.ContinuumCoulomb.MediatorListProgram.sourceBonds line 215
  52. def OAI.ContinuumCoulomb.MediatorListProgram.stage_certificate line 219