OAI/MathematicalPhysics/ContinuumCoulomb/Programs/ContactGeometryBlockProgram.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

Uniform polynomial-time serialization of the actual mediator vertex blocks: old vertices, first sites, second sites, and the two third-site blocks. The static local labels agree with ContactMediator.encodeSite.

  1. abbrev OAI.ContinuumCoulomb.ContactGeometryBlockProgram.EdgeInput line 14
  2. def OAI.ContinuumCoulomb.ContactGeometryBlockProgram.defaultEdge line 16
  3. def OAI.ContinuumCoulomb.ContactGeometryBlockProgram.pointCode line 18
  4. def OAI.ContinuumCoulomb.ContactGeometryBlockProgram.block line 20
  5. abbrev OAI.ContinuumCoulomb.ContactGeometryBlockProgram.LoopInput line 25
  6. def OAI.ContinuumCoulomb.ContactGeometryBlockProgram.loopCode line 27
  7. opaque OAI.ContinuumCoulomb.ContactGeometryBlockProgram.indexProgram line 30
  8. opaque OAI.ContinuumCoulomb.ContactGeometryBlockProgram.edgesProgram line 33
  9. opaque OAI.ContinuumCoulomb.ContactGeometryBlockProgram.quotientProgram line 36
  10. opaque OAI.ContinuumCoulomb.ContactGeometryBlockProgram.remainderProgram line 40
  11. opaque OAI.ContinuumCoulomb.ContactGeometryBlockProgram.edgeProgram line 44
  12. opaque OAI.ContinuumCoulomb.ContactGeometryBlockProgram.pointListProgram line 49
  13. opaque OAI.ContinuumCoulomb.ContactGeometryBlockProgram.stepProgram line 54
  14. opaque OAI.ContinuumCoulomb.ContactGeometryBlockProgram.blockProgram line 60
  15. def OAI.ContinuumCoulomb.ContactGeometryBlockProgram.firstSites line 73
  16. def OAI.ContinuumCoulomb.ContactGeometryBlockProgram.secondSites line 76
  17. def OAI.ContinuumCoulomb.ContactGeometryBlockProgram.thirdFirstSites line 81
  18. def OAI.ContinuumCoulomb.ContactGeometryBlockProgram.thirdSecondSites line 86
  19. def OAI.ContinuumCoulomb.ContactGeometryBlockProgram.oldPoint line 92
  20. opaque OAI.ContinuumCoulomb.ContactGeometryBlockProgram.oldPointProgram line 94
  21. abbrev OAI.ContinuumCoulomb.ContactGeometryBlockProgram.Input line 103
  22. def OAI.ContinuumCoulomb.ContactGeometryBlockProgram.inputCode line 105
  23. def OAI.ContinuumCoulomb.ContactGeometryBlockProgram.positions line 109
  24. opaque OAI.ContinuumCoulomb.ContactGeometryBlockProgram.oldProgram line 113
  25. opaque OAI.ContinuumCoulomb.ContactGeometryBlockProgram.listProgram line 117
  26. opaque OAI.ContinuumCoulomb.ContactGeometryBlockProgram.program line 121
  27. theorem OAI.ContinuumCoulomb.ContactGeometryBlockProgram.positions_length line 129
  28. def OAI.ContinuumCoulomb.ContactGeometryBlockProgram.certificate line 136