Two difference operators

Theorem 5.1 (thm:twofactor) of paper/nivat.tex. A primitive lattice basis puts the first direction on the horizontal axis. Lemma 5.5 selects and normalizes a low-cost boundary in the preimage of the original rectangle. The positive-height argument uses Lemmas 5.6–5.8; a one-row window uses the factorial common period from Corollary 5.3. Directional periods are transported back through both coordinate changes. The parallel case uses bounded finite differences. The final corollary treats sums of two periodic configurations.

theorem Nivat.TwoFactors.wordComplexity_row_le {A : Type u_1} (c : Configuration A) (hc : FiniteRange c) (e : ℕ) (j : ℤ) : wordComplexity (fun (i : ℤ) => c (i, j)) e ≤ complexity c (rowPrefix e)

The word complexity of any row is bounded by the configuration's horizontal-edge complexity, which counts translations on all rows. Theorem 5.1 (thm:twofactor), one-row case using Corollary 5.3 (cor:morse).

theorem Nivat.TwoFactors.isPeriod_factorial_of_lowcomplex_rowPrefix {A : Type u_1} (c : Configuration A) (hc : FiniteRange c) (e : ℕ) (he : 0 < e) (hlow : complexity c (rowPrefix e) ≤ e) : IsPeriod c (↑e.factorial, 0)

In the one-row case of Theorem 5.1 (thm:twofactor), Corollary 5.3 bounds every row period by the edge length, so its factorial is a period of all rows simultaneously.

theorem Nivat.TwoFactors.mixed_difference_neg_right {A : Type u_1} [AddCommGroup A] (c : Configuration A) (h t : Lattice) (hmix : difference h (difference t c) = 0) : difference h (difference (-t) c) = 0

Reversing the transverse direction preserves the mixed-difference identity, by commutation and negation of a period. Theorem 5.1 (thm:twofactor).

theorem Nivat.two_factors_nonparallel (c : Configuration ℚ) (hc : FiniteRange c) (m n : ℕ) (_hm : 0 < m) (_hn : 0 < n) (h t : Lattice) (hh : h ≠ 0) (_ht : t ≠ 0) (hcomplexity : complexity c (rectangle m n) ≤ m * n) (hmix : difference h (difference t c) = 0) (hparallel : h.1 * t.2 ≠ h.2 * t.1) : ∃ (k : ℤ), k ≠ 0 ∧ (IsPeriod c (k • h) ∨ IsPeriod c (k • t))

The directional conclusion of Theorem 5.1 (thm:twofactor): for nonparallel directions, a nonzero integer multiple of one of them is a period. The complexity bound is on the original axis-aligned rectangle.

theorem Nivat.two_factors (c : Configuration ℚ) (hc : FiniteRange c) (m n : ℕ) (hm : 0 < m) (hn : 0 < n) (h t : Lattice) (hh : h ≠ 0) (ht : t ≠ 0) (hcomplexity : complexity c (rectangle m n) ≤ m * n) (hmix : difference h (difference t c) = 0) : Periodic c

Theorem 5.1 (thm:twofactor). A finite-range rational configuration with at most m * n patterns on the original positive axis-aligned rectangle and annihilated by the product of two nonzero directional differences has a nonzero global period.

theorem Nivat.difference_add {A : Type u_1} [AddCommGroup A] (h : Lattice) (a b : Configuration A) : difference h (a + b) = difference h a + difference h b

Difference operators distribute over sums, the algebraic observation after Theorem 5.1 (thm:twofactor) that gives the two-periodic-summand corollary.

theorem Nivat.two_periodic_summands (c a b : Configuration ℚ) (hc : FiniteRange c) (hsum : c = a + b) (m n : ℕ) (hm : 0 < m) (hn : 0 < n) (h t : Lattice) (hh : h ≠ 0) (ht : t ≠ 0) (ha : IsPeriod a h) (hb : IsPeriod b t) (hlow : complexity c (rectangle m n) ≤ m * n) : Periodic c

The consequence of Theorem 5.1 stated in the opening discussion of Section 5 (sec:twofactor): a low-complexity finite-range sum of two periodic rational configurations is periodic. The individual summands need not have finite range.