From a normalized window to a directional period

The positive-height case in the proof of Theorem 5.1 (thm:twofactor) of paper/nivat.tex. Lemma 5.6 supplies either a transverse period or an agreeing strip with a boundary disagreement. Lemma 5.7 gives periodic interior rows in the latter case, and Lemma 5.8 extends a multiple of the horizontal direction to a global period. The conclusion retains which input direction supplies it.

theorem Nivat.TwoFactors.directional_period_of_short_window (c : Configuration ℚ) (hc : FiniteRange c) (C : Finset Lattice) (e H : ℕ) (hH : 0 < H) (hC : ∀ z ∈ C, 1 ≤ z.2 ∧ z.2 ≤ ↑H) (hblocks : ∀ (j : Fin H), ∃ (α : ℤ), ∀ s < e - 1, (α + ↑s, ↑↑j + 1) ∈ C) (hcost : complexity c (prefixWindow C e) < complexity c C + e) (q : ℕ) (hq : 0 < q) (a M : ℤ) (hM : 0 < M) (hmix : difference (↑q, 0) (difference (a, M) c) = 0) : ∃ (k : ℤ), k ≠ 0 ∧ (IsPeriod c (k • (↑q, 0)) ∨ IsPeriod c (k • (a, M)))

Theorem 5.1 (thm:twofactor), after the window of Lemma 5.5 has been normalized: a nonzero integer multiple of one of the two directions is a period. Lemmas 5.6–5.8 preserve which direction supplies the period.