Selecting a short boundary from a convex lattice window

The geometric part of Lemma 5.5 (lem:boundary-window) of paper/nivat.tex. Integer slices of convex sets are consecutive blocks. Rational interpolation and integer rounding give the sharp lower bound of e - 1 sites on intermediate rows. A low-complexity row band of least cardinality has positive discrepancy after either nonempty endpoint is deleted; choosing its shorter endpoint gives the boundary cost inequality. This finite minimization implements the lemma's discrepancy-crossing selection.

def Nivat.TwoFactors.LatticeConvex (D : Finset Lattice) : Prop

A finite set containing exactly the integer points of a convex subset of the rational plane; this includes rectangles expressed in an arbitrary lattice basis. Lemma 5.5 (lem:boundary-window).

Equations

• Nivat.TwoFactors.LatticeConvex D = ∃ (S : Set (ℚ × ℚ)), Convex ℚ S ∧ ∀ (z : Nivat.Lattice), z ∈ D ↔ Nivat.latticeRatCast z ∈ S

def Nivat.TwoFactors.RowBandSubset (D₀ D : Finset Lattice) : Prop

A subset retaining every original site between any two occupied row levels, as occurs when extreme rows are deleted. Lemma 5.5 (lem:boundary-window).

Equations

• Nivat.TwoFactors.RowBandSubset D₀ D = (D ⊆ D₀ ∧ ∀ z ∈ D₀, (∃ u ∈ D, u.2 ≤ z.2) → (∃ v ∈ D, z.2 ≤ v.2) → z ∈ D)

theorem Nivat.TwoFactors.RowBandSubset.refl (D : Finset Lattice) : RowBandSubset D D

The original finite window is a row band of itself, so it is an admissible initial window for discrepancy selection. Lemma 5.5 (lem:boundary-window).

theorem Nivat.TwoFactors.RowBandSubset.filter_gt {D₀ D : Finset Lattice} (hD : RowBandSubset D₀ D) (a : ℤ) : RowBandSubset D₀ ({z ∈ D | a < z.2})

Deleting all rows at or below a level preserves the property of retaining every original site between occupied rows. Lemma 5.5 (lem:boundary-window).

theorem Nivat.TwoFactors.RowBandSubset.filter_lt {D₀ D : Finset Lattice} (hD : RowBandSubset D₀ D) (b : ℤ) : RowBandSubset D₀ ({z ∈ D | z.2 < b})

Deleting all rows at or above a level preserves the property of retaining every original site between occupied rows. Lemma 5.5 (lem:boundary-window).

theorem Nivat.TwoFactors.exists_minimal_lowcomplex_rowBand {A : Type u_1} (c : Configuration A) (D₀ : Finset Lattice) (hlow : complexity c D₀ ≤ D₀.card) : ∃ (D : Finset Lattice), RowBandSubset D₀ D ∧ complexity c D ≤ D.card ∧ ∀ (E : Finset Lattice), RowBandSubset D₀ E → complexity c E ≤ E.card → D.card ≤ E.card

Among the row bands with nonpositive discrepancy, choose one of least cardinality; deleting an occupied extreme row from it must give positive discrepancy. Lemma 5.5 (lem:boundary-window).

theorem Nivat.TwoFactors.convex_horizontal_interval {S : Set (ℚ × ℚ)} (hS : Convex ℚ S) {l r t j : ℚ} (hl : (l, j) ∈ S) (hr : (r, j) ∈ S) (hlt : l ≤ t) (htr : t ≤ r) : (t, j) ∈ S

A convex subset of the rational plane contains the full horizontal interval between two points of the same row. Lemma 5.5 (lem:boundary-window).

theorem Nivat.TwoFactors.LatticeConvex.row_interval {D : Finset Lattice} (hD : LatticeConvex D) {l r t j : ℤ} (hl : (l, j) ∈ D) (hr : (r, j) ∈ D) (hlt : l ≤ t) (htr : t ≤ r) : (t, j) ∈ D

Every integer site between two sites in one row of a lattice-convex window belongs to that window. Lemma 5.5 (lem:boundary-window).

theorem Nivat.TwoFactors.LatticeConvex.row_interpolation {D : Finset Lattice} (hD : LatticeConvex D) (a b l₀ l₁ : ℤ) (e : ℕ) (he : 0 < e) (hab : a < b) (hbottom : ∀ r < e, (l₀ + ↑r, a) ∈ D) (htop : ∀ r < e, (l₁ + ↑r, b) ∈ D) (j : ℤ) (haj : a ≤ j) (hjb : j ≤ b) : ∃ (l : ℤ), ∀ r < e - 1, (l + ↑r, j) ∈ D

If both extreme rows have at least e consecutive sites, convex interpolation gives at least e - 1 consecutive integer sites on every intermediate row. Ceiling the interpolated left endpoint accounts for the sharp loss of one site. Lemma 5.5 (lem:boundary-window).

theorem Nivat.TwoFactors.latticeConvex_rectangle (m n : ℕ) : LatticeConvex (rectangle m n)

The integer sites of an axis-aligned rectangle are exactly the integer points in the corresponding convex rational rectangle. Lemma 5.5 (lem:boundary-window).

theorem Nivat.TwoFactors.LatticeConvex.linear_preimage {D₀ D : Finset Lattice} (hD₀ : LatticeConvex D₀) (φ : Lattice → Lattice) (L : ℚ × ℚ →ₗ[ℚ] ℚ × ℚ) (hcompat : ∀ (z : Lattice), latticeRatCast (φ z) = L (latticeRatCast z)) (hmem : ∀ (z : Lattice), z ∈ D ↔ φ z ∈ D₀) : LatticeConvex D

A compatible rational linear map pulls a lattice-convex window back to another lattice-convex window. The membership equation records the actual preimage in the chosen basis. Lemma 5.5 (lem:boundary-window).

def Nivat.TwoFactors.rowSites (D : Finset Lattice) (j : ℤ) : Finset Lattice

The sites of a finite window at a fixed row level. Lemma 5.5 (lem:boundary-window).

Equations

• Nivat.TwoFactors.rowSites D j = {z ∈ D | z.2 = j}

def Nivat.TwoFactors.rowCoordinates (D : Finset Lattice) (j : ℤ) : Finset ℤ

The horizontal integer coordinates of the sites at a fixed row level. Lemma 5.5 (lem:boundary-window).

Equations

• Nivat.TwoFactors.rowCoordinates D j = Finset.image Prod.fst (Nivat.TwoFactors.rowSites D j)

@[simp]

theorem Nivat.TwoFactors.mem_rowCoordinates (D : Finset Lattice) (j i : ℤ) : i ∈ rowCoordinates D j ↔ (i, j) ∈ D

An integer is a row coordinate exactly when its paired lattice point belongs to that row of the window. Lemma 5.5 (lem:boundary-window).

theorem Nivat.TwoFactors.card_rowCoordinates (D : Finset Lattice) (j : ℤ) : (rowCoordinates D j).card = (rowSites D j).card

Projection to the horizontal coordinate is injective within a fixed row and therefore preserves its number of sites. Lemma 5.5 (lem:boundary-window).

theorem Nivat.TwoFactors.RowBandSubset.row_interval {D₀ D : Finset Lattice} (hband : RowBandSubset D₀ D) (hD₀ : LatticeConvex D₀) {l r t j : ℤ} (hl : (l, j) ∈ D) (hr : (r, j) ∈ D) (hlt : l ≤ t) (htr : t ≤ r) : (t, j) ∈ D

An occupied row of a row band retains every site between any two of its sites, by row convexity of the original window. Lemma 5.5 (lem:boundary-window).

theorem Nivat.TwoFactors.row_exact_block {D : Finset Lattice} (j : ℤ) (hrow : ∀ (l r t : ℤ), (l, j) ∈ D → (r, j) ∈ D → l ≤ t → t ≤ r → (t, j) ∈ D) (hne : (rowCoordinates D j).Nonempty) : ∃ (l : ℤ), ∀ (i : ℤ), (i, j) ∈ D ↔ ∃ r < (rowCoordinates D j).card, i = l + ↑r

A nonempty finite integer row with no gaps consists exactly of a consecutive block whose length is its cardinality. Lemma 5.5 (lem:boundary-window).

theorem Nivat.TwoFactors.small_cost_of_minimal_rowBand_endpoint {A : Type u_1} (c : Configuration A) {D₀ D : Finset Lattice} (hband : RowBandSubset D₀ D) (hlow : complexity c D ≤ D.card) (hmin : ∀ (E : Finset Lattice), RowBandSubset D₀ E → complexity c E ≤ E.card → D.card ≤ E.card) (a : ℤ) (hend : (∀ z ∈ D, a ≤ z.2) ∨ ∀ z ∈ D, z.2 ≤ a) (hne : ∃ z ∈ D, z.2 = a) : complexity c D < complexity c ({z ∈ D | z.2 ≠ a}) + (rowSites D a).card

Deleting a nonempty endpoint row from a smallest low-complexity band crosses to positive discrepancy, so the increase in pattern count is smaller than the number of deleted sites. Lemma 5.5 (lem:boundary-window), equation eq:boundary-cost.

structure Nivat.TwoFactors.ShapeWindow {A : Type u_1} (c : Configuration A) (D₀ : Finset Lattice) : Type

The selected window before translation and normal reflection: an extreme consecutive edge, its interior, the boundary cost, and consecutive-block witnesses in every row. Lemma 5.5 (lem:boundary-window).

• D : Finset Lattice

  The selected row band inside the input window.

• C : Finset Lattice

  The interior obtained by deleting the selected extreme row.

• lo : ℤ

  The lowest row of the selected band.

• hi : ℤ

  The highest row of the selected band.

• edge : ℤ

  The row selected for deletion.

• start : ℤ

  The horizontal coordinate of the first edge site.

• e : ℕ

  The positive number of consecutive edge sites.

• band : RowBandSubset D₀ self.D

  All input sites between occupied rows are retained.

• ordered : self.lo ≤ self.hi

  The lower row does not exceed the upper row.

• bounds (z : Lattice) : z ∈ self.D → self.lo ≤ z.2 ∧ z.2 ≤ self.hi

  Every selected site lies between the extreme rows.

• edge_side : self.edge = self.lo ∨ self.edge = self.hi

  The selected edge is one of the two extreme rows.

• positive : 0 < self.e

  The selected edge is nonempty.

• edge_exact (i : ℤ) : (i, self.edge) ∈ self.D ↔ ∃ r < self.e, i = self.start + ↑r

  The selected edge is exactly the consecutive block of length e.

• edge_card : (rowSites self.D self.edge).card = self.e

  The edge length agrees with its finite-set cardinality.

• interior_eq : self.C = {z ∈ self.D | z.2 ≠ self.edge}

  The interior consists of all selected sites off the edge.

• low_complexity : complexity c self.D ≤ self.D.card

  The selected band has nonpositive discrepancy.

• small_cost : complexity c self.D < complexity c self.C + self.e

  The boundary pattern increase is less than the edge length.

• row_blocks (j : ℤ) : self.lo ≤ j → j ≤ self.hi → ∃ (l : ℤ), ∀ r < self.e - 1, (l + ↑r, j) ∈ self.D

  Every row of the band contains e - 1 consecutive sites.

theorem Nivat.TwoFactors.exists_shapeWindow {A : Type u_1} (c : Configuration A) (hc : FiniteRange c) (D₀ : Finset Lattice) (hconv : LatticeConvex D₀) (hlow₀ : complexity c D₀ ≤ D₀.card) : Nonempty (ShapeWindow c D₀)

A low-complexity lattice-convex window contains a row band with a shorter extreme edge whose deletion has cost less than the edge length and leaves the required e - 1 row blocks. Lemma 5.5 (lem:boundary-window).

theorem Nivat.TwoFactors.ShapeWindow.interior_row_blocks {A : Type u_1} {c : Configuration A} {D₀ : Finset Lattice} (w : ShapeWindow c D₀) (j : ℤ) (hlo : w.lo ≤ j) (hhi : j ≤ w.hi) (hne : j ≠ w.edge) : ∃ (l : ℤ), ∀ r < w.e - 1, (l + ↑r, j) ∈ w.C

At every row other than the selected extreme edge, the consecutive-block witnesses lie in the interior. Lemma 5.5 (lem:boundary-window).