Extending horizontal periodicity across rows

Lemma 5.8 (lem:row-lifting) of paper/nivat.tex. The boundary rule from Lemma 5.5 supplies the recurrence in Lemma 5.4. It makes finitely many further rows periodic. A common multiple of those row periods and the horizontal mixed-difference direction gives a difference vanishing on a full transverse fundamental strip; its transverse period then makes it vanish everywhere.

def Nivat.TwoFactors.RowPeriodic {A : Type u_1} (x : ℤ × ℤ → A) (j : ℤ) : Prop

A row has a positive integer period in the horizontal basis direction. Lemma 5.8 (lem:row-lifting).

Equations

• Nivat.TwoFactors.RowPeriodic x j = ∃ (p : ℕ), 0 < p ∧ Function.Periodic (fun (i : ℤ) => x (i, j)) ↑p

def Nivat.TwoFactors.BoundaryRule {A : Type u_1} (x : ℤ × ℤ → A) (C : Finset (ℤ × ℤ)) (k : ℕ) : Prop

Equal occurring interior patterns and equal first k boundary values determine the next boundary value, the rule in equation eq:boundary-rule. Lemma 5.5 (lem:boundary-window).

Equations

• Nivat.TwoFactors.BoundaryRule x C k = ∀ (z z' : ℤ × ℤ), (∀ u ∈ C, x (u + z) = x (u + z')) → (∀ (r : Fin k), x (z + (↑↑r, 0)) = x (z' + (↑↑r, 0))) → x (z + (↑k, 0)) = x (z' + (↑k, 0))

theorem Nivat.TwoFactors.common_period_of_finite {A : Type u_1} {ι : Type u_2} (s : Finset ι) (f : ι → ℤ → A) (h : ∀ i ∈ s, ∃ (p : ℕ), 0 < p ∧ Function.Periodic (f i) ↑p) : ∃ (p : ℕ), 0 < p ∧ ∀ i ∈ s, Function.Periodic (f i) ↑p

A finite family of periodic bilateral words has a common positive period, obtained by multiplying their periods. Lemma 5.8 (lem:row-lifting).

theorem Nivat.TwoFactors.eq_const_of_periodic_of_strip {A : Type u_1} (d : ℤ × ℤ → A) (a M b : ℤ) (hM : 0 < M) (ht : Function.Periodic d (a, M)) (s : A) (hz : ∀ (i j : ℤ), b ≤ j → j < b + M → d (i, j) = s) (z : ℤ × ℤ) : d z = s

A configuration periodic by (a,M), with M > 0, that is constant on any M consecutive rows is constant everywhere: division with remainder moves every point into those rows. Lemma 5.8 (lem:row-lifting).

theorem Nivat.TwoFactors.propagate_rows_downward (P : ℤ → Prop) (H : ℕ) (hinit : ∀ (j : ℤ), 1 ≤ j → j ≤ ↑H → P j) (hstep : ∀ (j : ℤ), (∀ (r : ℤ), 1 ≤ r → r ≤ ↑H → P (j + r)) → P j) (n : ℕ) (j : ℤ) : -↑n < j → j ≤ ↑H → P j

A property determined by the next H rows propagates downward through any prescribed finite number of rows. Lemma 5.8 (lem:row-lifting).

theorem Nivat.TwoFactors.interior_forcing_periodic {A : Type u_1} (x : ℤ × ℤ → A) (C : Finset (ℤ × ℤ)) (j : ℤ) (hrows : ∀ u ∈ C, RowPeriodic x (j + u.2)) : ∃ (p : ℕ), 0 < p ∧ Function.Periodic (fun (i : ℤ) (u : ↥C) => x (↑u + (i, j))) ↑p

If each of the finitely many rows supporting the translated interior pattern is periodic, their common period makes that pattern a periodic parameter. Lemma 5.8 (lem:row-lifting).

theorem Nivat.TwoFactors.rowPeriodic_of_boundaryRule {A : Type u_1} (x : ℤ × ℤ → A) (hx : (Set.range x).Finite) (C : Finset (ℤ × ℤ)) (k : ℕ) (hrule : BoundaryRule x C k) (j : ℤ) (hrows : ∀ u ∈ C, RowPeriodic x (j + u.2)) : RowPeriodic x j

A boundary row is periodic when its interior rows are periodic: the boundary rule and interior parameter satisfy the periodic-forcing lemma, including zero memory. Lemma 5.8 (lem:row-lifting), using Lemma 5.4 (lem:forcing).

theorem Nivat.TwoFactors.difference_multiple_period {A : Type u_1} [AddCommGroup A] (x : Configuration A) (h t : Lattice) (hmix : difference h (difference t x) = 0) (n : ℕ) : IsPeriod (difference (n • h) x) t

A vanishing mixed difference implies that the difference in a multiple of the first direction still has the second direction as a period. Commutation and multiples of a period give the operator consequence of equation eq:telescoping-lift. Lemma 5.8 (lem:row-lifting).

theorem Nivat.TwoFactors.periodic_of_rows_boundaryRule (x : Configuration ℚ) (hx : FiniteRange x) (C : Finset Lattice) (k H : ℕ) (_hH : 0 < H) (hC : ∀ u ∈ C, 1 ≤ u.2 ∧ u.2 ≤ ↑H) (hrule : BoundaryRule x C k) (q : ℕ) (_hq : 0 < q) (a M : ℤ) (hM : 0 < M) (hmix : difference (↑q, 0) (difference (a, M) x) = 0) (hrows : ∀ (j : ℤ), 1 ≤ j → j ≤ ↑H → RowPeriodic x j) : ∃ (L : ℕ), 0 < L ∧ IsPeriod x (↑(L * q), 0)

A boundary rule and periodic initial interior rows yield a global horizontal period that is a positive multiple of the supplied horizontal direction. Only finitely many row periods are combined; the transverse mixed difference extends their common multiple across the plane. Lemma 5.8 (lem:row-lifting).