Strict reduction of rectangular area

This module proves the geometry in Corollary 2.3 (cor:line-descent). The four coordinate extrema describe the eroded rectangle. Two distinct support sites force at least one side to shrink, so nonempty erosion has strictly smaller area.

The main interface exists_smaller_rectangle_of_annihilator obtains the two support sites directly from a nonzero annihilated configuration. This geometric statement holds for arbitrary Laurent filters; in the corollary it is applied to the line generator supplied by Theorem 4.1 (thm:exact-ideal). Nonemptiness and the filtered complexity inequality in Corollary 2.3 come from Nivat.Descent.exact_complexity_descent; the final rectangular induction combines them with the geometry proved here.

theorem Nivat.Algebra.exists_smaller_rectangle_of_erodedWindow_nonempty (Φ : Laurent) (hΦ : Φ ≠ 0) (m n : ℕ) (hS : (erodedWindow Φ hΦ (rectangle m n)).Nonempty) (htwo : ∃ u ∈ Φ.coeff.support, ∃ v ∈ Φ.coeff.support, u ≠ v) : ∃ (m' : ℕ) (n' : ℕ) (o : Lattice), 0 < m' ∧ 0 < n' ∧ m' * n' < m * n ∧ erodedWindow Φ hΦ (rectangle m n) = Finset.image (fun (z : Lattice) => z + o) (rectangle m' n')

The geometric reduction in Corollary 2.3 (cor:line-descent), stated for any filter with two distinct support sites: a nonempty erosion is a translated positive axis-aligned rectangle of strictly smaller area.

theorem Nivat.Algebra.exists_smaller_rectangle_of_annihilator (Φ : Laurent) (hΦ : Φ ≠ 0) (d : Configuration ℚ) (hd : d ≠ 0) (hann : act Φ d = 0) (m n : ℕ) (hS : (erodedWindow Φ hΦ (rectangle m n)).Nonempty) : ∃ (m' : ℕ) (n' : ℕ) (o : Lattice), 0 < m' ∧ 0 < n' ∧ m' * n' < m * n ∧ erodedWindow Φ hΦ (rectangle m n) = Finset.image (fun (z : Lattice) => z + o) (rectangle m' n')

The strict-area conclusion of Corollary 2.3 (cor:line-descent): annihilation of a nonzero configuration supplies the distinct support sites, and nonempty erosion is exactly a translated positive rectangle of smaller area.