OAI/Topology/CoarseAssembly/HexagonSides.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

The six oriented sides of the lattice hexagon

These explicit vertex sequences support the boundary-walk construction. They run counterclockwise from (j,0); only the final side crosses the half-open positive ray used by the integral charge.

  1. def OAI.CoarseAssembly.hexagonPoint line 14
  2. theorem OAI.CoarseAssembly.hexagonPoint_radius line 23
  3. def OAI.CoarseAssembly.hexagonVertex line 38
  4. theorem OAI.CoarseAssembly.hexagonPoint_adj line 42
  5. theorem OAI.CoarseAssembly.hexagonVertex_adj line 47
  6. theorem OAI.CoarseAssembly.hexagonPoint_charge line 51
  7. def OAI.CoarseAssembly.hexagonSideWalk line 60
  8. def OAI.CoarseAssembly.boundaryCharge line 66
  9. theorem OAI.CoarseAssembly.hexagonSideWalk_charge line 69
  10. def OAI.CoarseAssembly.hexagonCorner line 86
  11. theorem OAI.CoarseAssembly.hexagonSide_end line 89
  12. def OAI.CoarseAssembly.hexagonSide line 94
  13. theorem OAI.CoarseAssembly.hexagonSide_charge line 98
  14. theorem OAI.CoarseAssembly.hexagonCorner_zero line 105
  15. def OAI.CoarseAssembly.hexagonalWalk line 110
  16. theorem OAI.CoarseAssembly.hexagonalWalk_charge line 115
  17. def OAI.CoarseAssembly.hexagonalBoundaryWalks line 120