Documentation

LeanPool.Nivat.TwoFactors.BoundaryCounting

Boundary cost and unique extension #

The counting part of Lemma 5.5 (lem:boundary-window) and the fiber count in Lemma 5.7 (lem:periodic-interior) of paper/nivat.tex. Restriction is a surjection on occurring patterns. A small total increase forces a zero increase at one boundary site, and the total excess of fiber sizes bounds the number of interior patterns with more than one boundary extension.

source
def Nivat.TwoFactors.rowPrefix (k : ℕ) :
Finset Lattice

The first k consecutive sites of the horizontal boundary row. Lemma 5.5 (lem:boundary-window), equation eq:boundary-rule-domain.

Equations
Instances For
    source
    @[simp]
    theorem Nivat.TwoFactors.mem_rowPrefix (z : Lattice) (k : ℕ) :
    z ∈ rowPrefix k ↔ ∃ i < k, z = (↑i, 0)

    Membership in the horizontal boundary prefix means being its rth site for some natural index r < k. Lemma 5.5 (lem:boundary-window).

    source
    @[simp]
    theorem Nivat.TwoFactors.rowPrefix_zero :
    rowPrefix 0 = ∅

    A boundary prefix of length zero is empty, so a zero-memory rule uses only the interior. Lemma 5.5 (lem:boundary-window).

    source
    theorem Nivat.TwoFactors.rowPrefix_mono :
    Monotone rowPrefix

    Increasing the prefix length retains all previously adjoined boundary sites. Lemma 5.5 (lem:boundary-window).

    source
    def Nivat.TwoFactors.prefixWindow (C : Finset Lattice) (k : ℕ) :
    Finset Lattice

    The interior together with the first k boundary sites, the finite window denoted D_k in the paper. Lemma 5.5 (lem:boundary-window), equation eq:boundary-rule-domain.

    Equations
    Instances For
      source
      @[simp]
      theorem Nivat.TwoFactors.prefixWindow_zero (C : Finset Lattice) :
      prefixWindow C 0 = C

      Before any boundary sites are adjoined, the prefix window is exactly the interior. Lemma 5.5 (lem:boundary-window).

      source
      theorem Nivat.TwoFactors.prefixWindow_mono (C : Finset Lattice) :
      Monotone (prefixWindow C)

      The successive interior-plus-prefix windows are nested, hence their pattern complexities are nondecreasing. Lemma 5.5 (lem:boundary-window).

      source
      theorem Nivat.TwoFactors.exists_plateau_of_small_increase (p : ℕ → ℕ) (hp : Monotone p) (e : ℕ) (hcost : p e < p 0 + e) :
      ∃ k < e, p (k + 1) = p k

      A nondecreasing integer sequence whose total increase over e steps is less than e has an adjacent equality. Lemma 5.5 (lem:boundary-window).

      source
      theorem Nivat.TwoFactors.boundaryRule_of_small_cost {A : Type u_1} (c : Configuration A) (hc : FiniteRange c) (C : Finset Lattice) (e : ℕ) (hcost : complexity c (prefixWindow C e) < complexity c C + e) :
      ∃ k < e, BoundaryRule c C k

      A boundary cost smaller than its length yields an index k < e where the next site is uniquely determined by the occurring interior and prefix pattern. Lemma 5.5 (lem:boundary-window), equation eq:boundary-rule.

      source
      theorem Nivat.TwoFactors.ambiguous_output_budget {A : Type u_1} {B : Type u_2} (f : A → B) {P : Set A} (hP : P.Finite) {Q : Set B} (hQ : ∀ b ∈ Q, ∃ x ∈ P, ∃ y ∈ P, x ≠ y ∧ f x = b ∧ f y = b) :
      Q.ncard + (f '' P).ncard ≤ P.ncard

      Outputs with at least two distinct preimages are bounded in number by input cardinality minus output cardinality. The additive statement counts only finite occurring fibers. Lemma 5.7 (lem:periodic-interior).