Translation and separation of square grid cells

All separation statements concern real points, including nonintegral points on routes. The integer cell indices may be negative. A positive integer radius r gives cells of side 2 * r; in particular, radius 120 gives cells of side 240.

Main definitions

• Cslib.Orthogonal.translate: translate the listed integer points of a route.
• Cslib.Orthogonal.cellOrigin, Cslib.Orthogonal.openCell, Cslib.Orthogonal.closedCell: square cells of the integer grid, interpreted in the real plane.
• Cslib.Orthogonal.cellPort: the four side midpoints of a cell.

Main results

• Translation preserves continuous support, orthogonality, simplicity and wire length.
• An open cell is disjoint from every distinct closed cell.
• Equal ports of distinct cells are on opposite sides of adjacent cells.

References

These are elementary coordinate facts, independent of any SAT encoding or gadget.

def Cslib.Orthogonal.translate (v : Point) (r : Route) : Route

Translate every listed point by the same integer displacement.

theorem Cslib.Orthogonal.realPoint_add (a b : Point) : realPoint (a + b) = realPoint a + realPoint b

Integer translation agrees with real translation.

theorem Cslib.Orthogonal.mem_segment_translate_iff (v a b : Point) (p : ℝ × ℝ) : p + realPoint v ∈ segment (a + v) (b + v) ↔ p ∈ segment a b

Translation preserves membership in the entire continuous segment.

theorem Cslib.Orthogonal.mem_support_translate_iff (v : Point) (r : Route) (p : ℝ × ℝ) : p + realPoint v ∈ support (translate v r) ↔ p ∈ support r

Membership in a translated support is precisely translated membership.

theorem Cslib.Orthogonal.support_translate (v : Point) (r : Route) : support (translate v r) = (fun (p : ℝ × ℝ) => p + realPoint v) '' support r

Translation of a route translates its entire real support.

theorem Cslib.Orthogonal.axisAligned_add_iff (v a b : Point) : AxisAligned (a + v) (b + v) ↔ AxisAligned a b

Translation preserves proper axis alignment.

theorem Cslib.Orthogonal.isOrthogonal_translate_iff (v : Point) (r : Route) : IsOrthogonal (translate v r) ↔ IsOrthogonal r

Translation preserves orthogonality.

theorem Cslib.Orthogonal.length_add (v a b : Point) : length (a + v) (b + v) = length a b

Translation preserves Manhattan segment length.

theorem Cslib.Orthogonal.wireLength_translate (v : Point) (r : Route) : wireLength (translate v r) = wireLength r

Translation preserves total wire length.

theorem Cslib.Orthogonal.endpointContacts_add_iff (v a b c d : Point) : EndpointContacts (a + v) (b + v) (c + v) (d + v) ↔ EndpointContacts a b c d

Translation preserves endpoint-only contact certificates.

theorem Cslib.Orthogonal.isSimple_translate_iff (v : Point) (r : Route) : IsSimple (translate v r) ↔ IsSimple r

Translation preserves continuous simplicity.

def Cslib.Orthogonal.cellOrigin (r : ℤ) (c : Point) : Point

The lower-left corner of a square cell of side 2 * r.

def Cslib.Orthogonal.openCell (r : ℤ) (c : Point) : Set (ℝ × ℝ)

The open real square belonging to integer cell c.

def Cslib.Orthogonal.closedCell (r : ℤ) (c : Point) : Set (ℝ × ℝ)

The closed real square belonging to integer cell c.

theorem Cslib.Orthogonal.support_subset_openCell {r : ℤ} {c : Point} {a : Route} (h : ∀ q ∈ a, realPoint q ∈ openCell r c) : support a ⊆ openCell r c

Bounds on the listed vertices control the entire continuous support in an open cell.

theorem Cslib.Orthogonal.support_subset_closedCell {r : ℤ} {c : Point} {a : Route} (h : ∀ q ∈ a, realPoint q ∈ closedCell r c) : support a ⊆ closedCell r c

Bounds on the listed vertices control the entire continuous support in a closed cell.

theorem Cslib.Orthogonal.cell_eq_of_mem_open_closed {r : ℤ} (hr : 0 < r) {c d : Point} {p : ℝ × ℝ} (hc : p ∈ openCell r c) (hd : p ∈ closedCell r d) : c = d

A point in one open cell and another closed cell forces equal integer indices.

theorem Cslib.Orthogonal.disjoint_openCell_closedCell {r : ℤ} (hr : 0 < r) {c d : Point} (hcd : c ≠ d) : Disjoint (openCell r c) (closedCell r d)

Distinct cells have no real contact between an open cell and a closed cell.

theorem Cslib.Orthogonal.disjoint_openCell {r : ℤ} (hr : 0 < r) {c d : Point} (hcd : c ≠ d) : Disjoint (openCell r c) (openCell r d)

Distinct open cells are disjoint in the real plane.

def Cslib.Orthogonal.cellPort (r : ℤ) (c : Point) (s : Fin 4) : Point

Side midpoints, in order left, right, bottom, top.

theorem Cslib.Orthogonal.cellPort_eq_cases {r : ℤ} (hr : 0 < r) {c d : Point} {s t : Fin 4} (hcd : c ≠ d) (h : cellPort r c s = cellPort r d t) : s = 0 ∧ t = 1 ∧ d = c + (-1, 0) ∨ s = 1 ∧ t = 0 ∧ d = c + (1, 0) ∨ s = 2 ∧ t = 3 ∧ d = c + (0, -1) ∨ s = 3 ∧ t = 2 ∧ d = c + (0, 1)

Equal side midpoints in distinct cells identify the adjacent cell and opposite side. The displacements refer to the integer cell indices, not scaled drawing coordinates.

theorem Cslib.Orthogonal.realPoint_cellPort_eq_cases {r : ℤ} (hr : 0 < r) {c d : Point} {s t : Fin 4} (hcd : c ≠ d) (h : realPoint (cellPort r c s) = realPoint (cellPort r d t)) : s = 0 ∧ t = 1 ∧ d = c + (-1, 0) ∨ s = 1 ∧ t = 0 ∧ d = c + (1, 0) ∨ s = 2 ∧ t = 3 ∧ d = c + (0, -1) ∨ s = 3 ∧ t = 2 ∧ d = c + (0, 1)

The port classification also applies to equality in the real plane.

theorem Cslib.Orthogonal.mem_openCell_add_origin_iff (r : ℤ) (c : Point) (p : ℝ × ℝ) : p + realPoint (cellOrigin r c) ∈ openCell r c ↔ 0 < p.1 ∧ p.1 < ↑(2 * r) ∧ 0 < p.2 ∧ p.2 < ↑(2 * r)

Translating a point from the open local square puts it in the corresponding grid cell.

theorem Cslib.Orthogonal.mem_closedCell_add_origin_iff (r : ℤ) (c : Point) (p : ℝ × ℝ) : p + realPoint (cellOrigin r c) ∈ closedCell r c ↔ 0 ≤ p.1 ∧ p.1 ≤ ↑(2 * r) ∧ 0 ≤ p.2 ∧ p.2 ≤ ↑(2 * r)

Translating a point from the closed local square puts it in the corresponding grid cell.

theorem Cslib.Orthogonal.center_mem_openCell {r : ℤ} (hr : 0 < r) (c : Point) : realPoint (cellOrigin r c + (r, r)) ∈ openCell r c

Positive-radius cells have an interior center, at the translated point (r,r).

theorem Cslib.Orthogonal.disjoint_support_of_cells {r : ℤ} (hr : 0 < r) {c d : Point} (hcd : c ≠ d) {a b : Route} (ha : support a ⊆ openCell r c) (hb : support b ⊆ closedCell r d) : Disjoint (support a) (support b)

Route supports in distinct open/closed cells are disjoint, including nonintegral points.