Termination from bounds on least-color occurrences

A uniform capacity for each interval's least color turns the finite-color interval lemma into a uniform bound on operation-sequence length. The bound depends only on the number of colors and the capacity function.

def EGZ.HasIntervalCapacity (χ capacity : ℕ → ℕ) (N : ℕ) : Prop

Every interval before N has at most capacity a occurrences of any color which is a lower bound for all colors on that interval.

Equations

• EGZ.HasIntervalCapacity χ capacity N = ∀ (a b l : ℕ), a ≤ b → b < N → (∀ i ∈ Finset.Icc a b, l ≤ χ i) → {i ∈ Finset.Icc a b | χ i = l}.card ≤ capacity a

noncomputable def EGZ.intervalCapacityBound (k : ℕ) (capacity : ℕ → ℕ) : ℕ

The first length at which the interval lemma forces a capacity violation. The requested occurrence threshold is exactly capacity + 1.

Equations

• EGZ.intervalCapacityBound k capacity = Nat.find ⋯

theorem EGZ.intervalCapacityBound_spec (k : ℕ) (capacity χ : ℕ → ℕ) : (∀ i < intervalCapacityBound k capacity, χ i < k) → ∃ (a : ℕ) (b : ℕ) (l : ℕ), b < intervalCapacityBound k capacity ∧ l < k ∧ HasColorInterval χ (fun (a : ℕ) => capacity a + 1) a b l

theorem EGZ.length_lt_intervalCapacityBound (k : ℕ) (capacity : ℕ → ℕ) (N : ℕ) (χ : ℕ → ℕ) (hχ : ∀ i < N, χ i < k) (hcapacity : HasIntervalCapacity χ capacity N) : N < intervalCapacityBound k capacity

The bound is uniform over operation sequences; no monotonicity of the colors or of the capacity function is required.

theorem EGZ.exists_length_bound_of_interval_capacity (k : ℕ) (capacity : ℕ → ℕ) : ∃ (B : ℕ), ∀ (N : ℕ) (χ : ℕ → ℕ), (∀ i < N, χ i < k) → HasIntervalCapacity χ capacity N → N < B

Existential formulation of the uniform termination bound.