A coherent chain of mortal periodic masks

An arbitrary sequence of pencils can be handled under the abstract MaskMortality hypothesis. The masks are refined at every stage and the integral sparsity bound is retained. A pointwise choice then produces a nonzero sequence respecting every assignment at every stage.

def KoetheCounterexample.MaskSequence.Carries {k : Type u_1} [Field k] (M : PeriodicMask k) (w : List (Triple k)) : Prop

The word is installed at the beginning of a period, and fits in that period.

Equations

• KoetheCounterexample.MaskSequence.Carries M w = (w.length ≤ M.period ∧ ∀ (i : Fin w.length), M.lookup ↑i = some (w.get i))

def KoetheCounterexample.MaskSequence.Kills {k : Type u_1} [Field k] {d : ℕ} (M : PeriodicMask k) (P : Pencil k d) : Prop

A mask contains a periodically recurring mortal word for this pencil.

Equations

• KoetheCounterexample.MaskSequence.Kills M P = ∃ (w : List (KoetheCounterexample.Triple k)), KoetheCounterexample.MaskSequence.Carries M w ∧ P.wordProd w = 0

@[reducible, inline]

abbrev KoetheCounterexample.MaskSequence.SparseMask (k : Type u_2) [Field k] : Type u_2

Finite masks whose assigned density is strictly less than one quarter.

Equations

• KoetheCounterexample.MaskSequence.SparseMask k = { M : KoetheCounterexample.PeriodicMask k // 4 * M.assigned < M.period }

theorem KoetheCounterexample.MaskSequence.exists_mortal_extension {k : Type u_1} [Field k] (hm : MaskMortality k) (M : SparseMask k) {d : ℕ} (P : Pencil k d) : ∃ (N : SparseMask k), Extends ↑N ↑M ∧ (↑M).period ∣ (↑N).period ∧ Kills (↑N) P

Apply mortality only to a mask with more than half its positions free, then preserve every old assignment while installing the resulting word.

def KoetheCounterexample.MaskSequence.masks {k : Type u_1} [Field k] (hm : MaskMortality k) (e : ℕ → (d : ℕ) × Pencil k d) : ℕ → SparseMask k

Stage zero has no assignments. Stage j+1 additionally kills pencil e j.

Equations

• KoetheCounterexample.MaskSequence.masks hm e 0 = ⟨KoetheCounterexample.MaskSequence.emptyMask, ⋯⟩
• KoetheCounterexample.MaskSequence.masks hm e j.succ = ⋯.choose

theorem KoetheCounterexample.MaskSequence.masks_succ {k : Type u_1} [Field k] (hm : MaskMortality k) (e : ℕ → (d : ℕ) × Pencil k d) (j : ℕ) : Extends ↑(masks hm e (j + 1)) ↑(masks hm e j) ∧ (↑(masks hm e j)).period ∣ (↑(masks hm e (j + 1))).period ∧ Kills (↑(masks hm e (j + 1))) (e j).snd

theorem KoetheCounterexample.MaskSequence.masks_extends {k : Type u_1} [Field k] (hm : MaskMortality k) (e : ℕ → (d : ℕ) × Pencil k d) {i j : ℕ} (hij : i ≤ j) : Extends ↑(masks hm e j) ↑(masks hm e i)

theorem KoetheCounterexample.MaskSequence.masks_period_dvd {k : Type u_1} [Field k] (hm : MaskMortality k) (e : ℕ → (d : ℕ) × Pencil k d) {i j : ℕ} (hij : i ≤ j) : (↑(masks hm e i)).period ∣ (↑(masks hm e j)).period

theorem KoetheCounterexample.MaskSequence.exists_compatible_sequence {k : Type u_1} [Field k] (M : ℕ → PeriodicMask k) (hM : ∀ (i j : ℕ), i ≤ j → Extends (M j) (M i)) : ∃ (v : ℕ → Triple k), (∀ (n : ℕ), v n ≠ 0) ∧ ∀ (j : ℕ), (M j).SeqCompatible v

Any increasing chain of nonzero partial masks has a simultaneous nonzero completion. A site assigned at any stage retains that exact vector forever. Sites that are never assigned can harmlessly be filled with a fixed nonzero vector; consequently no assertion about the density of the infinite union is required.

theorem KoetheCounterexample.MaskSequence.exists_sequence_for_enumeration {k : Type u_1} [Field k] (hm : MaskMortality k) (e : ℕ → (d : ℕ) × Pencil k d) : ∃ (v : ℕ → Triple k), (∀ (n : ℕ), v n ≠ 0) ∧ ∀ (j : ℕ), (↑(masks hm e j)).SeqCompatible v

A nonzero sequence respecting all the periodic mortal words in the chain.