A product of difference operators from a nonzero annihilator

Proposition 3.3 (prop:product) is exists_product_differences_of_annihilator. Appendix A (app:product) proves it by separate integer scaling of the configuration and filter, prime dilation, and polynomial interpolation. Every output direction is nonzero, and the resulting list of difference factors is nonempty.

The action coefficientAct is defined over a commutative coefficient ring so that reduction from integers to ZMod p commutes with filtering. Frobenius identifies the prime power of a reduced filter with dilation of its exponents. A common bound on all dilated integer outputs then forces sufficiently large prime dilations of annihilators to annihilate. Factorization extends this to the progression 1 + j * B! in equation (eq:dilation-family).

The theorem dilation_interpolation_identity is equation (eq:interpolation) with an arbitrary auxiliary polynomial. Translating one nonzero coefficient to exponent zero and choosing factors C(M) - X isolates that coefficient and gives a product of M - 1. Casting back to rationals and cancelling the nonzero scaling factors concludes the proof.

def Nivat.Algebra.coefficientShift {R : Type u_1} [CommRing R] (h : Lattice) : Module.End R (Configuration R)

Auxiliary to Proposition 3.3 (prop:product), Appendix A (app:product): a forward translation as a linear endomorphism over the coefficient ring.

Equations

• Nivat.Algebra.coefficientShift h = { toFun := Nivat.shift h, map_add' := ⋯, map_smul' := ⋯ }

def Nivat.Algebra.coefficientShiftRepresentation {R : Type u_1} [CommRing R] : Multiplicative Lattice →* Module.End R (Configuration R)

Auxiliary to Proposition 3.3 (prop:product), Appendix A (app:product): the integer lattice acts by forward translations over a commutative ring.

Equations

• Nivat.Algebra.coefficientShiftRepresentation = { toFun := fun (h : Multiplicative Nivat.Lattice) => Nivat.Algebra.coefficientShift (Multiplicative.toAdd h), map_one' := ⋯, map_mul' := ⋯ }

noncomputable def Nivat.Algebra.coefficientActionHom {R : Type u_1} [CommRing R] : AddMonoidAlgebra R Lattice →ₐ[R] Module.End R (Configuration R)

Auxiliary to Proposition 3.3 (prop:product), Appendix A (app:product): extend the coefficient-ring shift representation to a Laurent algebra action.

Equations

• Nivat.Algebra.coefficientActionHom = (AddMonoidAlgebra.lift R (Module.End R (Nivat.Configuration R)) Nivat.Lattice) Nivat.Algebra.coefficientShiftRepresentation

noncomputable def Nivat.Algebra.coefficientAct {R : Type u_1} [CommRing R] (f : AddMonoidAlgebra R Lattice) (c : Configuration R) : Configuration R

Auxiliary to Proposition 3.3 (prop:product), Appendix A (app:product): the Laurent operator over a commutative ring, permitting both integral coefficients and reduction modulo a prime.

Equations

• Nivat.Algebra.coefficientAct f c = (Nivat.Algebra.coefficientActionHom f) c

theorem Nivat.Algebra.coefficientAct_apply {R : Type u_1} [CommRing R] (f : AddMonoidAlgebra R Lattice) (c : Configuration R) (z : Lattice) : coefficientAct f c z = f.coeff.sum fun (h : Lattice) (a : R) => a * c (z + h)

Auxiliary to Proposition 3.3 (prop:product), Appendix A (app:product): the coefficient-ring action is the finite sum of coefficients times translated values.

@[simp]

theorem Nivat.Algebra.coefficientAct_zero {R : Type u_1} [CommRing R] (c : Configuration R) : coefficientAct 0 c = 0

Auxiliary to Proposition 3.3 (prop:product), Appendix A (app:product): the zero coefficient-ring filter has zero output.

@[simp]

theorem Nivat.Algebra.coefficientAct_one {R : Type u_1} [CommRing R] (c : Configuration R) : coefficientAct 1 c = c

Auxiliary to Proposition 3.3 (prop:product), Appendix A (app:product): the identity coefficient-ring filter acts identically.

@[simp]

theorem Nivat.Algebra.coefficientAct_config_zero {R : Type u_1} [CommRing R] (f : AddMonoidAlgebra R Lattice) : coefficientAct f 0 = 0

Auxiliary to Proposition 3.3 (prop:product), Appendix A (app:product): every coefficient-ring filter annihilates the zero configuration.

theorem Nivat.Algebra.coefficientAct_add {R : Type u_1} [CommRing R] (f g : AddMonoidAlgebra R Lattice) (c : Configuration R) : coefficientAct (f + g) c = coefficientAct f c + coefficientAct g c

Auxiliary to Proposition 3.3 (prop:product), Appendix A (app:product): adding coefficient-ring filters adds their outputs.

theorem Nivat.Algebra.coefficientAct_mul {R : Type u_1} [CommRing R] (f g : AddMonoidAlgebra R Lattice) (c : Configuration R) : coefficientAct (f * g) c = coefficientAct f (coefficientAct g c)

Auxiliary to Proposition 3.3 (prop:product), Appendix A (app:product): multiplying coefficient-ring filters composes their actions.

theorem Nivat.Algebra.coefficientAct_finset_sum {R : Type u_1} [CommRing R] {ι : Type u_3} (S : Finset ι) (f : ι → AddMonoidAlgebra R Lattice) (c : Configuration R) : coefficientAct (∑ j ∈ S, f j) c = ∑ j ∈ S, coefficientAct (f j) c

Auxiliary to Proposition 3.3 (prop:product), Appendix A (app:product): the action of a finite filter sum is the corresponding sum of outputs.

@[simp]

theorem Nivat.Algebra.coefficientAct_single {R : Type u_1} [CommRing R] (h : Lattice) (a : R) (c : Configuration R) : coefficientAct (AddMonoidAlgebra.single h a) c = a • shift h c

Auxiliary to Proposition 3.3 (prop:product), Appendix A (app:product): a single coefficient acts as a scaled forward shift over the coefficient ring.

theorem Nivat.Algebra.coefficientAct_rat (f : Laurent) (c : Configuration ℚ) : coefficientAct f c = act f c

Auxiliary to Proposition 3.3 (prop:product), Appendix A (app:product): the general coefficient-ring action agrees with the rational action from Section 1.1.

theorem Nivat.Algebra.coefficientAct_map {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (ρ : R →+* S) (f : AddMonoidAlgebra R Lattice) (c : Configuration R) : coefficientAct ((AddMonoidAlgebra.mapRingHom Lattice ρ) f) (⇑ρ ∘ c) = ⇑ρ ∘ coefficientAct f c

Auxiliary to Proposition 3.3 (prop:product), Appendix A (app:product): changing the coefficient ring commutes with the action on the configuration, in particular for reduction modulo a prime.

def Nivat.Algebra.dilationLattice (n : ℕ) : Lattice →+ Lattice

Auxiliary to Proposition 3.3 (prop:product), Appendix A (app:product): natural scaling of lattice exponents as an additive homomorphism.

Equations

• Nivat.Algebra.dilationLattice n = { toFun := fun (h : Nivat.Lattice) => n • h, map_zero' := ⋯, map_add' := ⋯ }

noncomputable def Nivat.Algebra.dilate {R : Type u_1} [CommRing R] (n : ℕ) : AddMonoidAlgebra R Lattice →+* AddMonoidAlgebra R Lattice

Auxiliary to Proposition 3.3 (prop:product), Appendix A (app:product): the Laurent ring homomorphism scaling all lattice exponents by a natural number.

Equations

• Nivat.Algebra.dilate n = AddMonoidAlgebra.mapDomainRingHom R (Nivat.Algebra.dilationLattice n)

@[simp]

theorem Nivat.Algebra.dilate_single {R : Type u_1} [CommRing R] (n : ℕ) (h : Lattice) (a : R) : (dilate n) (AddMonoidAlgebra.single h a) = AddMonoidAlgebra.single (n • h) a

Auxiliary to Proposition 3.3 (prop:product), Appendix A (app:product): dilation scales the exponent of a single coefficient without changing that coefficient.

@[simp]

theorem Nivat.Algebra.dilate_one {R : Type u_1} [CommRing R] (f : AddMonoidAlgebra R Lattice) : (dilate 1) f = f

Auxiliary to Proposition 3.3 (prop:product), Appendix A (app:product): dilation by one fixes the filter.

theorem Nivat.Algebra.dilate_dilate {R : Type u_1} [CommRing R] (m n : ℕ) (f : AddMonoidAlgebra R Lattice) : (dilate m) ((dilate n) f) = (dilate (m * n)) f

Auxiliary to Proposition 3.3 (prop:product), Appendix A (app:product): composition of dilations multiplies their scaling parameters.

theorem Nivat.Algebra.map_dilate {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (ρ : R →+* S) (n : ℕ) (f : AddMonoidAlgebra R Lattice) : (AddMonoidAlgebra.mapRingHom Lattice ρ) ((dilate n) f) = (dilate n) ((AddMonoidAlgebra.mapRingHom Lattice ρ) f)

Auxiliary to Proposition 3.3 (prop:product), Appendix A (app:product): a coefficient-ring homomorphism commutes with dilation of the exponents.

theorem Nivat.Algebra.coefficientAct_pow_eq_zero {R : Type u_1} [CommRing R] (f : AddMonoidAlgebra R Lattice) (c : Configuration R) (hf : coefficientAct f c = 0) {n : ℕ} (hn : 0 < n) : coefficientAct (f ^ n) c = 0

Auxiliary to Proposition 3.3 (prop:product), Appendix A (app:product): every positive power of an annihilator still annihilates the configuration.

theorem Nivat.Algebra.finite_dilate_values {R : Type u_1} [CommRing R] (f : AddMonoidAlgebra R Lattice) {c : Configuration R} (hc : FiniteRange c) : (Set.range fun (nz : ℕ × Lattice) => coefficientAct ((dilate nz.1) f) c nz.2).Finite

Auxiliary to Proposition 3.3 (prop:product), Appendix A (app:product): a fixed finite filter on a finite-range configuration has finitely many outputs across all dilation exponents and lattice sites.

theorem Nivat.Algebra.zmod_pow_eq_dilate (p : ℕ) [Fact (Nat.Prime p)] (f : AddMonoidAlgebra (ZMod p) Lattice) : f ^ p = (dilate p) f

Auxiliary to Proposition 3.3 (prop:product), Appendix A (app:product): Frobenius in characteristic p identifies the pth power of a Laurent filter over ZMod p with its dilation by p.

theorem Nivat.Algebra.exists_uniform_dilate_bound (f : IntegerLaurent) {c : Configuration ℤ} (hc : FiniteRange c) : ∃ (B : ℕ), ∀ (n : ℕ) (z : Lattice), (coefficientAct ((dilate n) f) c z).natAbs ≤ B

Auxiliary to Proposition 3.3 (prop:product), Appendix A (app:product): the finite set of all dilated integer outputs has a common natural absolute-value bound.

theorem Nivat.Algebra.prime_dilate_annihilates (f : IntegerLaurent) (c : Configuration ℤ) (B : ℕ) (hbound : ∀ (n : ℕ) (z : Lattice), (coefficientAct ((dilate n) f) c z).natAbs ≤ B) {m p : ℕ} (hp : Nat.Prime p) (hBp : B < p) (hm : coefficientAct ((dilate m) f) c = 0) : coefficientAct ((dilate (m * p)) f) c = 0

Auxiliary to Proposition 3.3 (prop:product), Appendix A (app:product): dilation by a prime larger than the common output bound preserves annihilation. Frobenius makes each output divisible by that prime, and the strict absolute-value bound forces zero.

theorem Nivat.Algebra.coprime_dilate_annihilates (f : IntegerLaurent) (c : Configuration ℤ) (B : ℕ) (hbound : ∀ (n : ℕ) (z : Lattice), (coefficientAct ((dilate n) f) c z).natAbs ≤ B) (hf : coefficientAct f c = 0) {n : ℕ} (hn : 0 < n) (hcop : n.Coprime B.factorial) : coefficientAct ((dilate n) f) c = 0

Auxiliary to Proposition 3.3 (prop:product), Appendix A (app:product): prime factorization extends preservation of annihilation to every positive exponent coprime to the factorial bound.

theorem Nivat.Algebra.progression_dilate_annihilates (f : IntegerLaurent) (c : Configuration ℤ) (B : ℕ) (hbound : ∀ (n : ℕ) (z : Lattice), (coefficientAct ((dilate n) f) c z).natAbs ≤ B) (hf : coefficientAct f c = 0) (j : ℕ) : coefficientAct ((dilate (1 + j * B.factorial)) f) c = 0

Auxiliary to Proposition 3.3 (prop:product), Appendix A (app:product): equation (eq:dilation-family): all dilations at exponents 1 + j * B! annihilate.

theorem Nivat.Algebra.dilation_interpolation_identity {R : Type u_1} [CommRing R] (r : ℕ) (f : AddMonoidAlgebra R Lattice) (H : Polynomial (AddMonoidAlgebra R Lattice)) : (H.sum fun (j : ℕ) (b : AddMonoidAlgebra R Lattice) => b * (dilate (1 + j * r)) f) = ∑ h ∈ f.coeff.support, AddMonoidAlgebra.single h (f.coeff h) * Polynomial.eval (AddMonoidAlgebra.single (r • h) 1) H

Auxiliary to Proposition 3.3 (prop:product), Appendix A (app:product): equation (eq:interpolation): linear combinations of dilations along an arithmetic progression are evaluations of the coefficient polynomial at the corresponding lattice monomials.

theorem Nivat.Algebra.integer_centered_product (f : IntegerLaurent) (hf0 : f.coeff 0 ≠ 0) (c : Configuration ℤ) (hc : FiniteRange c) (hf : coefficientAct f c = 0) : ∃ (r : ℕ), 0 < r ∧ coefficientAct (∏ h ∈ f.coeff.support.erase 0, (AddMonoidAlgebra.single (r • h) 1 - 1)) c = 0

Auxiliary to Proposition 3.3 (prop:product), Appendix A (app:product): interpolation for an integral annihilator with nonzero constant coefficient produces a product of nonzero-exponent difference factors. The auxiliary factors C(M) - X evaluate at one to M - 1.

theorem Nivat.Algebra.exists_integer_product_differences {c : Configuration ℤ} (hc : FiniteRange c) (hcne : c ≠ 0) {f : IntegerLaurent} (hfne : f ≠ 0) (hf : coefficientAct f c = 0) : ∃ (hs : List Lattice), hs ≠ [] ∧ (∀ h ∈ hs, h ≠ 0) ∧ coefficientAct (List.map (fun (h : Lattice) => AddMonoidAlgebra.single h 1 - 1) hs).prod c = 0

Auxiliary to Proposition 3.3 (prop:product), Appendix A (app:product): translate a nonzero coefficient to exponent zero and apply interpolation. Nonzeroness of the configuration forces a nonempty factor list, and positive dilation preserves each nonzero direction.

theorem Nivat.Algebra.exists_product_differences_of_annihilator {c : Configuration ℚ} (hc : FiniteRange c) (hcne : c ≠ 0) {f : Laurent} (hfne : f ≠ 0) (hf : act f c = 0) : ∃ (hs : List Lattice), hs ≠ [] ∧ (∀ h ∈ hs, h ≠ 0) ∧ act (List.map (fun (h : Lattice) => monomial h - 1) hs).prod c = 0

Proposition 3.3 (prop:product), proved in Appendix A (app:product): every nonzero finite-range rational configuration with a nonzero Laurent annihilator has a nonempty product of differences in nonzero lattice directions as an annihilator.