Normalizing the selected boundary

The coordinate normalization in Lemma 5.5 (lem:boundary-window) of paper/nivat.tex. Translation places the first edge site at the origin, and reflection in the normal coordinate places the interior above the edge. The window and configuration are transported by the same affine bijection; the pattern inequality and row-block witnesses are preserved explicitly.

def Nivat.TwoFactors.normalSignEquiv (ε : ℤ) (hε : ε = 1 ∨ ε = -1) : Lattice ≃+ Lattice

The additive lattice equivalence that preserves horizontal coordinates and either preserves or reverses the normal coordinate. Lemma 5.5 (lem:boundary-window).

Equations

• Nivat.TwoFactors.normalSignEquiv ε hε = { toFun := fun (z : Nivat.Lattice) => (z.1, ε * z.2), invFun := fun (z : Nivat.Lattice) => (z.1, ε * z.2), left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }

def Nivat.TwoFactors.normalAffineEquiv (ε : ℤ) (hε : ε = 1 ∨ ε = -1) (start edge : ℤ) : Lattice ≃ Lattice

The affine lattice bijection sending the normalized edge origin to its selected site and choosing the normal orientation. Lemma 5.5 (lem:boundary-window).

Equations

• Nivat.TwoFactors.normalAffineEquiv ε hε start edge = (Nivat.TwoFactors.normalSignEquiv ε hε).trans (Equiv.addRight (start, edge))

@[simp]

theorem Nivat.TwoFactors.normalAffineEquiv_apply (ε : ℤ) (hε : ε = 1 ∨ ε = -1) (start edge : ℤ) (z : Lattice) : (normalAffineEquiv ε hε start edge) z = (z.1 + start, ε * z.2 + edge)

The normalization map translates the horizontal coordinate and translates the signed normal coordinate. Lemma 5.5 (lem:boundary-window).

theorem Nivat.TwoFactors.normalAffineEquiv_add (ε : ℤ) (hε : ε = 1 ∨ ε = -1) (start edge : ℤ) (z u : Lattice) : (normalAffineEquiv ε hε start edge) (z + u) = (normalAffineEquiv ε hε start edge) z + (normalSignEquiv ε hε) u

The linear part of the affine normalization transports a translation vector by the chosen normal sign. Lemma 5.5 (lem:boundary-window).

structure Nivat.TwoFactors.NormalizedWindow {A : Type u_1} (c : Configuration A) : Type

The bottom-edge window data together with the exact affine change of configuration under which its boundary-cost inequality holds. Lemma 5.5 (lem:boundary-window).

• s : Lattice ≃ Lattice

  The affine map from normalized sites to the selected window sites.

• t : Lattice ≃+ Lattice

  The additive linear part transporting period vectors.

• affine (z u : Lattice) : self.s (z + u) = self.s z + self.t u

  Translation vectors are transported by the linear part.

• horizontal (q : ℤ) : self.t (q, 0) = (q, 0)

  The horizontal coordinate direction is fixed by normalization.

• C : Finset Lattice

  The normalized interior above the bottom edge.

• e : ℕ

  The number of sites on the normalized bottom edge.

• H : ℕ

  The highest normalized interior row, allowing zero.

• positive : 0 < self.e

  The bottom edge has positive length.

• interior (z : Lattice) : z ∈ self.C → 1 ≤ z.2 ∧ z.2 ≤ ↑self.H

  All interior sites lie on rows 1 through H.

• blocks (j : Fin self.H) : ∃ (l : ℤ), ∀ r < self.e - 1, (l + ↑r, ↑↑j + 1) ∈ self.C

  Each interior row contains e - 1 consecutive sites.

• cost : complexity (c ∘ ⇑self.s) (prefixWindow self.C self.e) < complexity (c ∘ ⇑self.s) self.C + self.e

  The transported configuration satisfies the strict boundary-cost inequality.

theorem Nivat.TwoFactors.ShapeWindow.normalize {A : Type u_1} {c : Configuration A} {D₀ : Finset Lattice} (w : ShapeWindow c D₀) : Nonempty (NormalizedWindow c)

Translate the first edge site to the origin and orient the normal coordinate so that the interior lies above it, preserving the actual pattern inequality and row-block witnesses. Lemma 5.5 (lem:boundary-window).