Bounded configurations with vanishing higher differences

This module proves Lemma 3.4 (lem:repeated) of paper/nivat.tex and the parallel case of Theorem 5.1. Boundedness rules out a nonzero affine slope along a lattice orbit; boundedness of differences then reduces every positive order to the first difference.

The main results are difference_eq_zero_of_iterate_of_bounded, its finite-range specialization difference_eq_zero_of_iterate, and periodic_of_parallel_mixed_difference. Finite-range closure lemmas also support the orbit-closure difference in Corollary 3.6 (cor:periodic-difference).

theorem Nivat.FiniteRange.sub {A : Type u_1} [Sub A] {c d : Configuration A} (hc : FiniteRange c) (hd : FiniteRange d) : FiniteRange (c - d)

Pointwise subtraction preserves finite range, as needed for the orbit-closure difference in Corollary 3.6 (cor:periodic-difference).

theorem Nivat.FiniteRange.difference {A : Type u_1} [AddCommGroup A] {c : Configuration A} (hc : FiniteRange c) (h : Lattice) : FiniteRange (Nivat.difference h c)

A directional difference preserves finite range, as used when applying Lemma 3.4 (lem:repeated).

theorem Nivat.difference_eq_zero_of_second_of_bounded (c : Configuration ℚ) (B : ℚ) (hc : ∀ (z : Lattice), |c z| ≤ B) (h : Lattice) (h2 : difference h (difference h c) = 0) : difference h c = 0

A bounded rational configuration with zero second difference has zero first difference: a nonzero affine slope would contradict its uniform absolute bound. This is the affine-sequence step in Lemma 3.4 (lem:repeated).

theorem Nivat.FiniteRange.exists_abs_le {c : Configuration ℚ} (hc : FiniteRange c) : ∃ (B : ℚ), ∀ (z : Lattice), |c z| ≤ B

A finite rational range has a uniform absolute bound, as needed to apply Lemma 3.4 (lem:repeated) to finite-range configurations.

theorem Nivat.difference_eq_zero_of_second (c : Configuration ℚ) (hc : FiniteRange c) (h : Lattice) (h2 : difference h (difference h c) = 0) : difference h c = 0

A finite-range rational configuration with zero second difference has zero first difference. This is the affine-sequence case of Lemma 3.4 (lem:repeated).

theorem Nivat.abs_difference_le (c : Configuration ℚ) (B : ℚ) (hc : ∀ (z : Lattice), |c z| ≤ B) (h z : Lattice) : |difference h c z| ≤ 2 * B

A uniform absolute bound on a rational configuration bounds each first difference by twice that bound. This preserves boundedness during the reduction of difference order in Lemma 3.4 (lem:repeated).

theorem Nivat.difference_eq_zero_of_iterate_of_bounded (c : Configuration ℚ) (B : ℚ) (hc : ∀ (z : Lattice), |c z| ≤ B) (h : Lattice) (s : ℕ) (hs : 0 < s) (hpow : (difference h)^[s] c = 0) : difference h c = 0

Lemma 3.4 (lem:repeated): a bounded rational configuration annihilated by a positive iterate of a difference is annihilated by the first difference. The direction may also be zero, when the conclusion is immediate.

theorem Nivat.difference_eq_zero_of_iterate (c : Configuration ℚ) (hc : FiniteRange c) (h : Lattice) (s : ℕ) (hs : 0 < s) (hpow : (difference h)^[s] c = 0) : difference h c = 0

A finite-range rational configuration annihilated by a positive iterate of a directional difference is annihilated by its first difference. This is the finite-range specialization of Lemma 3.4 (lem:repeated).

theorem Nivat.difference_eq_zero_of_mixed_common_multiple (c : Configuration ℚ) (hc : FiniteRange c) (h t : Lattice) (hmix : difference h (difference t c) = 0) (a b : ℤ) (hab : a • h = b • t) : difference (a • h) c = 0

A common integer multiple of two mixed-difference directions is a period of a finite-range rational configuration. This is the repeated-difference argument in the parallel case of Theorem 5.1; the integer coefficients may have either sign.

theorem Nivat.periodic_of_parallel_mixed_difference (c : Configuration ℚ) (hc : FiniteRange c) (h t : Lattice) (hh : h ≠ 0) (ht : t ≠ 0) (hparallel : h.1 * t.2 = h.2 * t.1) (hmix : difference h (difference t c) = 0) : Periodic c

The parallel case of Theorem 5.1: two nonzero parallel directions with vanishing mixed difference force periodicity of a finite-range rational configuration. This case needs no complexity hypothesis.