Matching paired boundaries of grid cells

Main results

• boundary_eq_cases: equal boundary points in distinct cells determine adjacent opposite sides and the same lane.
• boundary_not_mem_openCell: a paired boundary belongs to no open grid cell.

References

These are original integer-coordinate facts about the fixed paired-port interface.

theorem Cslib.Orthogonal.PairedPorts.boundary_eq_cases {c d : Point} {s t : Fin 4} {l k : Fin 2} (hcd : c ≠ d) (h : cellOrigin 120 c + boundaryPort s l = cellOrigin 120 d + boundaryPort t k) : l = k ∧ d = c + neighbor s ∧ t = oppositeSide s

Equal boundary points in distinct cells identify the lane and opposite adjacent sides.

theorem Cslib.Orthogonal.PairedPorts.boundary_mem_closedCell (c : Point) (s : Fin 4) (l : Fin 2) : realPoint (cellOrigin 120 c + boundaryPort s l) ∈ closedCell 120 c

Each translated paired boundary belongs to its own closed cell.

theorem Cslib.Orthogonal.PairedPorts.boundary_not_mem_openCell (c d : Point) (s : Fin 4) (l : Fin 2) : realPoint (cellOrigin 120 c + boundaryPort s l) ∉ openCell 120 d

A translated paired boundary lies outside every open grid cell.