A period tangent to a vanishing half-plane

This module proves Proposition 3.5 (prop:tangent-period) and Corollary 3.6 (cor:periodic-difference) of paper/nivat.tex. Transverse differences are injective on configurations vanishing below some normal threshold. Cancelling them from a product annihilator leaves only tangent directions; a common multiple and Lemma 3.4 then give a period.

The main results are exists_tangent_period_of_nonzero_annihilator and periodic_difference_of_nonzero_annihilator. The latter combines the tangent period with Lemma 3.1 and the pattern inheritance of Section 1.1.

def Nivat.Dynamics.normalHom (ν : ℝ × ℝ) : Lattice →+ ℝ

The additive normal coordinate ν · z used in Proposition 3.5 (prop:tangent-period).

Equations

• Nivat.Dynamics.normalHom ν = { toFun := fun (z : Nivat.Lattice) => ν.1 * ↑z.1 + ν.2 * ↑z.2, map_zero' := ⋯, map_add' := ⋯ }

def Nivat.Dynamics.ZeroBelow (ν : ℝ × ℝ) (d : Configuration ℚ) : Prop

The vanishing space V_ν in Proposition 3.5 (prop:tangent-period): a configuration vanishes below some normal threshold, which may depend on the configuration.

Equations

• Nivat.Dynamics.ZeroBelow ν d = ∃ (B : ℝ), ∀ (z : Nivat.Lattice), (Nivat.Dynamics.normalHom ν) z < B → d z = 0

theorem Nivat.Dynamics.ZeroBelow.shift {ν : ℝ × ℝ} {d : Configuration ℚ} (hd : ZeroBelow ν d) (h : Lattice) : ZeroBelow ν (Nivat.shift h d)

The vanishing space V_ν is preserved by every shift after adjusting its threshold, as required for transverse cancellation in Proposition 3.5 (prop:tangent-period).

theorem Nivat.Dynamics.ZeroBelow.sub {ν : ℝ × ℝ} {d e : Configuration ℚ} (hd : ZeroBelow ν d) (he : ZeroBelow ν e) : ZeroBelow ν (d - e)

The vanishing space V_ν is closed under subtraction, using the smaller of the two thresholds in Proposition 3.5 (prop:tangent-period).

theorem Nivat.Dynamics.ZeroBelow.difference {ν : ℝ × ℝ} {d : Configuration ℚ} (hd : ZeroBelow ν d) (h : Lattice) : ZeroBelow ν (Nivat.difference h d)

Every directional difference preserves the vanishing space V_ν of Proposition 3.5 (prop:tangent-period).

theorem Nivat.Dynamics.zero_of_zeroBelow_periodic_pos {ν : ℝ × ℝ} {d : Configuration ℚ} (hd : ZeroBelow ν d) (h : Lattice) (hpos : 0 < (normalHom ν) h) (hp : IsPeriod d h) : d = 0

A periodic configuration in V_ν is zero when its period has positive normal coordinate: each orbit reaches the vanishing half-plane. This is the injectivity argument of Proposition 3.5 (prop:tangent-period).

theorem Nivat.Dynamics.zero_of_zeroBelow_difference {ν : ℝ × ℝ} {d : Configuration ℚ} (hd : ZeroBelow ν d) (h : Lattice) (htrans : (normalHom ν) h ≠ 0) (hdiff : difference h d = 0) : d = 0

A transverse difference has trivial kernel on V_ν, for either sign of its normal coordinate. This is the cancellation principle of Proposition 3.5 (prop:tangent-period).

theorem Nivat.Dynamics.act_eq_zero_of_origin_language (c x : Configuration ℚ) (hx : ∀ (D : Finset Lattice), patternAt x D 0 ∈ patterns c D) (f : Laurent) (hf : Algebra.act f c = 0) : Algebra.act f x = 0

Finite-pattern language inclusion transports each Laurent annihilator, by evaluating its translated finite support. This is equation eq:inheritance in Section 1.1, used in Corollary 3.6 (cor:periodic-difference).

noncomputable def Nivat.Dynamics.differenceProduct (hs : List Lattice) : Laurent

The Laurent product of directional difference factors appearing in Proposition 3.5 (prop:tangent-period), including any repeated directions.

Equations

• Nivat.Dynamics.differenceProduct hs = (List.map (fun (h : Nivat.Lattice) => Nivat.Algebra.monomial h - 1) hs).prod

@[simp]

theorem Nivat.Dynamics.differenceProduct_nil : differenceProduct [] = 1

The empty product of difference factors is the identity, so cancelling every factor forces the configuration to vanish in Proposition 3.5 (prop:tangent-period).

@[simp]

theorem Nivat.Dynamics.differenceProduct_cons (h : Lattice) (hs : List Lattice) : differenceProduct (h :: hs) = (Algebra.monomial h - 1) * differenceProduct hs

Prepending a direction multiplies its difference factor into the product used in Proposition 3.5 (prop:tangent-period).

theorem Nivat.Dynamics.act_differenceProduct_cons (h : Lattice) (hs : List Lattice) (d : Configuration ℚ) : Algebra.act (differenceProduct (h :: hs)) d = difference h (Algebra.act (differenceProduct hs) d)

The action of a product beginning with a direction is that directional difference of the remaining action, as used in Proposition 3.5 (prop:tangent-period).

theorem Nivat.Dynamics.ZeroBelow.act_differenceProduct {ν : ℝ × ℝ} {d : Configuration ℚ} (hd : ZeroBelow ν d) (hs : List Lattice) : ZeroBelow ν (Algebra.act (differenceProduct hs) d)

A finite product of difference operators preserves V_ν, which justifies iterated cancellation in Proposition 3.5 (prop:tangent-period).

theorem Nivat.Dynamics.cancel_transverse_factors {ν : ℝ × ℝ} (hs : List Lattice) (d : Configuration ℚ) (hd : ZeroBelow ν d) (hprod : Algebra.act (differenceProduct hs) d = 0) : Algebra.act (differenceProduct (List.filter (fun (h : Lattice) => decide ((normalHom ν) h = 0)) hs)) d = 0

Every transverse factor can be cancelled from an annihilating product on V_ν, retaining tangential factors with their multiplicities. This is the first step of Proposition 3.5 (prop:tangent-period).

theorem Nivat.Dynamics.normal_in_basis (ν : ℝ × ℝ) (e : Lattice ≃+ Lattice) (z : Lattice) : (normalHom ν) (e z) = ↑z.1 * (normalHom ν) (e (1, 0)) + ↑z.2 * (normalHom ν) (e (0, 1))

The normal coordinate in an integer lattice basis is the linear combination of its two basis values, as used for coordinate normalization in Proposition 3.5 (prop:tangent-period).

theorem Nivat.Dynamics.exists_oriented_tangent_basis (ν : ℝ × ℝ) (hν : ν ≠ 0) (h : Lattice) (hh : h ≠ 0) (htangent : (normalHom ν) h = 0) : ∃ (e : Lattice ≃+ Lattice), (normalHom ν) (e (1, 0)) = 0 ∧ 0 < (normalHom ν) (e (0, 1))

A tangential nonzero lattice vector and a nonzero normal admit an integer lattice basis whose first vector is tangent and whose second vector has positive normal coordinate. This is the basis choice in Proposition 3.5 (prop:tangent-period).

theorem Nivat.Dynamics.tangent_coordinate_zero (ν : ℝ × ℝ) (e : Lattice ≃+ Lattice) (hcol₁ : (normalHom ν) (e (1, 0)) = 0) (hcol₂ : 0 < (normalHom ν) (e (0, 1))) (h : Lattice) (htangent : (normalHom ν) h = 0) : (e.symm h).2 = 0

Tangential lattice vectors have zero transverse coordinate in an oriented tangent basis, as used in Proposition 3.5 (prop:tangent-period).

theorem Nivat.Dynamics.iterate_difference_eq_zero_of_common_multiple (hs : List Lattice) (H : Lattice) (hcommon : ∀ h ∈ hs, ∃ (k : ℤ), H = k • h) (d : Configuration ℚ) (hprod : Algebra.act (differenceProduct hs) d = 0) : (difference H)^[hs.length] d = 0

An annihilating product of directional differences implies a repeated difference in any common multiple of those directions. This is the operator-divisibility step of Proposition 3.5 (prop:tangent-period).

theorem Nivat.Dynamics.exists_common_multiple_on_basis_line (e : Lattice ≃+ Lattice) (hs : List Lattice) (hnonzero : ∀ h ∈ hs, h ≠ 0) (hline : ∀ h ∈ hs, (e.symm h).2 = 0) : ∃ (K : ℤ), K ≠ 0 ∧ ∀ h ∈ hs, ∃ (k : ℤ), e (K, 0) = k • h

Finitely many nonzero integer directions on a basis line have a common nonzero integer multiple, obtained from the product of their first coordinates in Proposition 3.5 (prop:tangent-period).

theorem Nivat.Dynamics.periodic_of_tangential_product (e : Lattice ≃+ Lattice) (hs : List Lattice) (hne : hs ≠ []) (hnonzero : ∀ h ∈ hs, h ≠ 0) (hline : ∀ h ∈ hs, (e.symm h).2 = 0) (d : Configuration ℚ) (hd : FiniteRange d) (hprod : Algebra.act (differenceProduct hs) d = 0) : ∃ (q : ℕ), 0 < q ∧ IsPeriod d (e (↑q, 0))

A finite-range rational configuration annihilated by a nonempty product of tangential differences has a positive period on that basis line. This is the final use of Lemma 3.4 (lem:repeated) in Proposition 3.5 (prop:tangent-period).

theorem Nivat.Dynamics.exists_tangent_period_of_nonzero_annihilator (d : Configuration ℚ) (hd : FiniteRange d) (hdne : d ≠ 0) (ν : ℝ × ℝ) (hν : ν ≠ 0) (hbelow : ∀ (z : Lattice), (normalHom ν) z < 0 → d z = 0) (f : Laurent) (hf : f ≠ 0) (hann : Algebra.act f d = 0) : ∃ (e : Lattice ≃+ Lattice) (q : ℕ), 0 < q ∧ (normalHom ν) (e (1, 0)) = 0 ∧ 0 < (normalHom ν) (e (0, 1)) ∧ IsPeriod d (e (↑q, 0))

Proposition 3.5 (prop:tangent-period): a nonzero finite-range rational configuration with a nonzero annihilator and vanishing on a half-plane has a positive period in a primitive tangent direction. The returned lattice basis also orients the transverse coordinate toward the positive half-plane.

theorem Nivat.Dynamics.periodic_difference_of_nonzero_annihilator (c : Configuration ℚ) (hc : FiniteRange c) (hn : ¬Periodic c) (f : Laurent) (hf : f ≠ 0) (hann : Algebra.act f c = 0) : ∃ (x : Configuration ℚ) (y : Configuration ℚ) (e : Lattice ≃+ Lattice) (q : ℕ), FiniteRange x ∧ FiniteRange y ∧ (∀ (D : Finset Lattice), patternAt x D 0 ∈ patterns c D) ∧ (∀ (D : Finset Lattice), patternAt y D 0 ∈ patterns c D) ∧ x - y ≠ 0 ∧ 0 < q ∧ IsPeriod (x - y) (e (↑q, 0)) ∧ ∀ b < 0, ∀ (a : ℤ), (x - y) (e (a, b)) = 0

Corollary 3.6 (cor:periodic-difference): a nonperiodic finite-range rational configuration with a nonzero annihilator yields a nonzero periodic difference of two configurations in its pattern language, vanishing on the negative rows of a primitive lattice basis.