OAI/Topology/CoarseAssembly/BoundaryWalks.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Boundary walks and their canonical lifts

Depth-zero fibers are singletons, so every edge of the actual boundary subgraph has its unique lift. The walk construction and charge comparison here leave only the explicit hexagonal boundary walk to be supplied.

  1. def OAI.CoarseAssembly.BoundaryComponent line 19
  2. instance OAI.CoarseAssembly.(instance at line 21) line 21
  3. def OAI.CoarseAssembly.boundaryGraph line 24
  4. def OAI.CoarseAssembly.boundaryRoot line 27
  5. def OAI.CoarseAssembly.boundaryFiberEmbedding line 29
  6. theorem OAI.CoarseAssembly.boundaryFiber_adj line 33
  7. def OAI.CoarseAssembly.boundaryFiberHom line 48
  8. def OAI.CoarseAssembly.boundaryBaseHom line 53
  9. theorem OAI.CoarseAssembly.walkCharge_map line 56
  10. theorem OAI.CoarseAssembly.walkCharge_copy line 63
  11. theorem OAI.CoarseAssembly.boundary_walk_charge line 69
  12. structure OAI.CoarseAssembly.HexagonalBoundaryWalks line 78

    Source documentation

    Geometric data still to be constructed from the six sides of the hexagon. These are own-paper obligations, not a published-input interface.

    structure HexagonalBoundaryWalks where
…
  13. def OAI.CoarseAssembly.HexagonalBoundaryWalks.fiberWalk line 84
  14. theorem OAI.CoarseAssembly.HexagonalBoundaryWalks.fiber_charge_one line 89