OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/ContactGeometryBlockSemantics.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

The serialized blocks are the original iterated graph's vertex array, through the explicit site permutation. No graph relabeling is assumed.

  1. theorem OAI.ContinuumCoulomb.ContactGeometryBlockProgram.lookup_ofFn line 13
  2. theorem OAI.ContinuumCoulomb.ContactGeometryBlockProgram.block_ofFn line 18
  3. def OAI.ContinuumCoulomb.ContactGeometryBlockProgram.literalEdge line 38
  4. def OAI.ContinuumCoulomb.ContactGeometryBlockProgram.literalInput line 44
  5. theorem OAI.ContinuumCoulomb.ContactGeometryBlockProgram.literal_position line 48
  6. theorem OAI.ContinuumCoulomb.ContactGeometryBlockProgram.literal_old line 56
  7. theorem OAI.ContinuumCoulomb.ContactGeometryBlockProgram.literal_length line 62
  8. def OAI.ContinuumCoulomb.ContactGeometryBlockProgram.firstIndex line 68
  9. def OAI.ContinuumCoulomb.ContactGeometryBlockProgram.secondIndex line 71
  10. def OAI.ContinuumCoulomb.ContactGeometryBlockProgram.thirdFirstIndex line 75
  11. def OAI.ContinuumCoulomb.ContactGeometryBlockProgram.thirdSecondIndex line 79
  12. theorem OAI.ContinuumCoulomb.ContactGeometryBlockProgram.firstIndex_val line 84
  13. theorem OAI.ContinuumCoulomb.ContactGeometryBlockProgram.secondIndex_val line 90
  14. theorem OAI.ContinuumCoulomb.ContactGeometryBlockProgram.thirdFirstIndex_val line 96
  15. theorem OAI.ContinuumCoulomb.ContactGeometryBlockProgram.thirdSecondIndex_val line 102
  16. theorem OAI.ContinuumCoulomb.ContactGeometryBlockProgram.first_block line 109
  17. theorem OAI.ContinuumCoulomb.ContactGeometryBlockProgram.second_block line 117
  18. theorem OAI.ContinuumCoulomb.ContactGeometryBlockProgram.thirdFirst_block line 125
  19. theorem OAI.ContinuumCoulomb.ContactGeometryBlockProgram.thirdSecond_block line 134
  20. theorem OAI.ContinuumCoulomb.ContactGeometryBlockProgram.literal_blocks line 145