An annihilator from low pattern complexity

The finite-range form of Lemma 3.2 (lem:ann-exists) is proved by affine dependence among the occurring patterns. exists_affine_annihilator gives a nonzero filter with constant output, and exists_nonzero_annihilator multiplies it by a nonzero difference.

The windowPolynomial linear map identifies finite coefficient vectors with Laurent polynomials supported in the window. Its injectivity, support, action, and reconstruction lemmas also supply the finite-dimensional pairing used in Theorem 2.2 (thm:descent).

noncomputable def Nivat.Algebra.windowPolynomial (D : Finset Lattice) (a : ↥D → ℚ) : Laurent

Auxiliary construction for Lemma 3.2 (lem:ann-exists): identify a coefficient vector on a finite window with its supported Laurent polynomial.

Equations

• Nivat.Algebra.windowPolynomial D a = ∑ z : ↥D, AddMonoidAlgebra.single (↑z) (a z)

theorem Nivat.Algebra.windowPolynomial_coeff (D : Finset Lattice) (a : ↥D → ℚ) (z : ↥D) : (windowPolynomial D a).coeff ↑z = a z

Auxiliary construction for Lemma 3.2 (lem:ann-exists): the supported polynomial recovers each input coefficient on the window.

theorem Nivat.Algebra.windowPolynomial_injective (D : Finset Lattice) : Function.Injective (windowPolynomial D)

Auxiliary construction for Lemma 3.2 (lem:ann-exists): the coefficient-vector identification is injective.

theorem Nivat.Algebra.windowPolynomial_support (D : Finset Lattice) (a : ↥D → ℚ) : (windowPolynomial D a).coeff.support ⊆ D

Auxiliary construction for Lemma 3.2 (lem:ann-exists): the polynomial associated with a window vector is supported inside that window.

theorem Nivat.Algebra.act_windowPolynomial (D : Finset Lattice) (a : ↥D → ℚ) (c : Configuration ℚ) (u : Lattice) : act (windowPolynomial D a) c u = ∑ z : ↥D, a z * c (u + ↑z)

Auxiliary construction for Lemma 3.2 (lem:ann-exists): the associated Laurent action is the coefficient pairing with a translated restriction.

theorem Nivat.Algebra.windowPolynomial_reconstruct (D : Finset Lattice) (f : Laurent) (hf : f.coeff.support ⊆ D) : (windowPolynomial D fun (z : ↥D) => f.coeff ↑z) = f

Auxiliary construction for Lemma 3.2 (lem:ann-exists): restriction of a supported polynomial followed by reconstruction returns that polynomial.

noncomputable def Nivat.Algebra.windowPolynomialLinear (D : Finset Lattice) : (↥D → ℚ) →ₗ[ℚ] Laurent

Auxiliary construction for Lemma 3.2 (lem:ann-exists): the supported-polynomial identification as a rational linear map.

Equations

• Nivat.Algebra.windowPolynomialLinear D = { toFun := Nivat.Algebra.windowPolynomial D, map_add' := ⋯, map_smul' := ⋯ }

theorem Nivat.Algebra.exists_affine_annihilator (c : Configuration ℚ) (hc : FiniteRange c) (D : Finset Lattice) (hlow : complexity c D ≤ D.card) : ∃ (g : Laurent), g ≠ 0 ∧ g.coeff.support ⊆ D ∧ ∃ (κ : ℚ), act g c = fun (x : Lattice) => κ

Auxiliary construction for Lemma 3.2 (lem:ann-exists): affine dependence among the occurring patterns gives a nonzero supported filter with constant output.

theorem Nivat.Algebra.exists_nonzero_annihilator (c : Configuration ℚ) (hc : FiniteRange c) (D : Finset Lattice) (hlow : complexity c D ≤ D.card) : ∃ (f : Laurent), f ≠ 0 ∧ act f c = 0

Lemma 3.2 (lem:ann-exists): low complexity gives a nonzero Laurent annihilator. A nonzero difference polynomial annihilates the constant output of the affine relation.