Universal mortal sequences from abstract mask mortality

This file supplies the combinatorial implication from MaskMortality k to a single nonzero sequence with uniformly vanishing windows for every pencil. The only matrix facts used are the forward concatenation law for wordProd and absorption by zero. There are no algebraic-geometric hypotheses beyond the abstract mortality assumption, and no assertion about the density of an infinite union of masks.

theorem KoetheCounterexample.MaskSequence.window_add {k : Type u_1} [Field k] {d : ℕ} (P : Pencil k d) (v : ℕ → Triple k) (start a b : ℕ) : P.window v start (a + b) = P.window v start a * P.window v (start + a) b

Split a forward window at a specified length.

theorem KoetheCounterexample.MaskSequence.window_eq_zero_of_subwindow {k : Type u_1} [Field k] {d : ℕ} (P : Pencil k d) (v : ℕ → Triple k) (start N offset len : ℕ) (hfit : offset + len ≤ N) (hz : P.window v (start + offset) len = 0) : P.window v start N = 0

A window containing a zero contiguous subwindow is itself zero. No commutation or rearrangement of the matrix factors is used.

theorem KoetheCounterexample.MaskSequence.carries_window {k : Type u_1} [Field k] {d : ℕ} (P : Pencil k d) (M : PeriodicMask k) {w : List (Triple k)} (hw : Carries M w) {v : ℕ → Triple k} (hv : M.SeqCompatible v) {b : ℕ} (hb : b % M.period = 0) : P.window v b w.length = P.wordProd w

An installed word occurs at every nonnegative multiple of the mask period in every compatible sequence.

theorem KoetheCounterexample.MaskSequence.kills_windows {k : Type u_1} [Field k] {d : ℕ} (P : Pencil k d) (M : PeriodicMask k) {v : ℕ → Triple k} (hv : M.SeqCompatible v) (hkill : Kills M P) (start : ℕ) : P.window v start (2 * M.period) = 0

Twice the mask period is one bound that works at every starting site.

theorem KoetheCounterexample.exists_universalMortalSequence (k : Type u_1) [Field k] [Countable k] (hm : MaskMortality k) : ∃ (v : ℕ → Triple k), UniversalMortalSequence k v

The complete combinatorial construction, independent of any proof of matrix mortality. Countability is used only to enumerate all pencils.