Pencils, periodic masks and mortality

The shared vocabulary of the mortality argument: a pencil is a matrix of homogeneous linear forms in three letters, affine in one central parameter whose coefficient is supported in the distinguished root row; its evaluation at letter vectors, its lift along three elements of an algebra, forward word products and windows of a letter sequence. A periodic mask fixes nonzero letters at some residues and leaves the others free. MaskMortality is the matrix-mortality property proved in LeanPool.Koethe.Mortality.MaskMortality, and UniversalMortalSequence is the target of the construction in LeanPool.Koethe.MaskSequence.Universal.

@[reducible, inline]

abbrev KoetheCounterexample.Triple (k : Type u_1) : Type u_1

A letter: a vector of three coefficients, one for each generator.

Equations

• KoetheCounterexample.Triple k = (Fin 3 → k)

structure KoetheCounterexample.Pencil (k : Type u_1) [Field k] (d : ℕ) : Type u_1

A homogeneous three-letter pencil, affine in one central parameter, whose parameter coefficient is supported in the distinguished row.

• scalar : Fin 3 → Matrix (Fin (d + 1)) (Fin (d + 1)) k

  The coefficient matrix of each letter in the parameter-free part.

• linear : Fin 3 → Matrix (Fin (d + 1)) (Fin (d + 1)) k

  The coefficient matrix of each letter multiplying the central parameter.

• linear_off_root (i : Fin 3) (row col : Fin (d + 1)) : row ≠ 0 → self.linear i row col = 0

theorem KoetheCounterexample.Pencil.ext {k : Type u_1} [Field k] {d : ℕ} {P Q : Pencil k d} (hc : P.scalar = Q.scalar) (hl : P.linear = Q.linear) : P = Q

theorem KoetheCounterexample.Pencil.ext_iff {k : Type u_1} [Field k] {d : ℕ} {P Q : Pencil k d} : P = Q ↔ P.scalar = Q.scalar ∧ P.linear = Q.linear

instance KoetheCounterexample.Pencil.instCountable {k : Type u_1} [Field k] {d : ℕ} [Countable k] : Countable (Pencil k d)

noncomputable def KoetheCounterexample.Pencil.eval {k : Type u_1} [Field k] {d : ℕ} (P : Pencil k d) (v : Triple k) : Matrix (Fin (d + 1)) (Fin (d + 1)) (Polynomial k)

Evaluation at a constant letter vector.

Equations

• P.eval v row col = Polynomial.C (∑ i : Fin 3, v i * P.scalar i row col) + Polynomial.X * Polynomial.C (∑ i : Fin 3, v i * P.linear i row col)

noncomputable def KoetheCounterexample.Pencil.lift {k : Type u_1} [Field k] {d : ℕ} {R : Type u_2} [Ring R] [Algebra k R] (P : Pencil k d) (a : Fin 3 → R) : Matrix (Fin (d + 1)) (Fin (d + 1)) (Polynomial R)

Evaluation at three elements of an arbitrary algebra.

Equations

• P.lift a row col = Polynomial.C (∑ i : Fin 3, (algebraMap k R) (P.scalar i row col) * a i) + Polynomial.X * Polynomial.C (∑ i : Fin 3, (algebraMap k R) (P.linear i row col) * a i)

noncomputable def KoetheCounterexample.Pencil.wordProd {k : Type u_1} [Field k] {d : ℕ} (P : Pencil k d) (w : List (Triple k)) : Matrix (Fin (d + 1)) (Fin (d + 1)) (Polynomial k)

Forward chronological multiplication. This is the transfer convention for backward shifts (a_i u)(n) = v_n(i) u(n+1).

Equations

• P.wordProd w = (List.map P.eval w).prod

@[simp]

theorem KoetheCounterexample.Pencil.wordProd_nil {k : Type u_1} [Field k] {d : ℕ} (P : Pencil k d) : P.wordProd [] = 1

@[simp]

theorem KoetheCounterexample.Pencil.wordProd_append {k : Type u_1} [Field k] {d : ℕ} (P : Pencil k d) (u w : List (Triple k)) : P.wordProd (u ++ w) = P.wordProd u * P.wordProd w

noncomputable def KoetheCounterexample.Pencil.window {k : Type u_1} [Field k] {d : ℕ} (P : Pencil k d) (v : ℕ → Triple k) (start len : ℕ) : Matrix (Fin (d + 1)) (Fin (d + 1)) (Polynomial k)

The forward product of the pencil along len consecutive letters of v from start.

Equations

• P.window v start len = P.wordProd (List.ofFn fun (i : Fin len) => v (start + ↑i))

structure KoetheCounterexample.PeriodicMask (k : Type u_1) [Field k] : Type u_1

A finite periodic collection of assigned nonzero letter vectors. Unassigned occurrences of a residue remain independent choices.

• period : ℕ

  The period of the mask.

• period_pos : 0 < self.period

  The period is positive.

• value : Fin self.period → Option (Triple k)

  The letter assigned at each residue, or none if the residue is free.

• nonzero (i : Fin self.period) (v : Triple k) : self.value i = some v → v ≠ 0

  Every assigned letter is nonzero.

def KoetheCounterexample.PeriodicMask.lookup {k : Type u_1} [Field k] (M : PeriodicMask k) (n : ℕ) : Option (Triple k)

The assignment of the mask at a site, read off its residue.

Equations

• M.lookup n = M.value ⟨n % M.period, ⋯⟩

noncomputable def KoetheCounterexample.PeriodicMask.holes {k : Type u_1} [Field k] (M : PeriodicMask k) : ℕ

The number of free residues in one period.

Equations

• M.holes = {i : Fin M.period | M.value i = none}.card

noncomputable def KoetheCounterexample.PeriodicMask.assigned {k : Type u_1} [Field k] (M : PeriodicMask k) : ℕ

The number of assigned residues in one period.

Equations

• M.assigned = {i : Fin M.period | M.value i ≠ none}.card

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

A word agrees with the mask at every assigned position it covers.

Equations

• M.Compatible w = ∀ (i : Fin w.length) (z : KoetheCounterexample.Triple k), M.lookup ↑i = some z → w.get i = z

def KoetheCounterexample.PeriodicMask.SeqCompatible {k : Type u_1} [Field k] (M : PeriodicMask k) (v : ℕ → Triple k) : Prop

A sequence agrees with the mask at every assigned site.

Equations

• M.SeqCompatible v = ∀ (n : ℕ) (z : KoetheCounterexample.Triple k), M.lookup n = some z → v n = z

def KoetheCounterexample.MaskMortality (k : Type u_1) [Field k] : Prop

The algebraic matrix-mortality property needed by the mask construction.

Equations

• One or more equations did not get rendered due to their size.

def KoetheCounterexample.UniversalMortalSequence (k : Type u_1) [Field k] (v : ℕ → Triple k) : Prop

A nonvanishing edge sequence killing every one-row pencil on uniformly bounded windows. Nil bounds are permitted to depend on the pencil.

Equations

• KoetheCounterexample.UniversalMortalSequence k v = ((∀ (n : ℕ), v n ≠ 0) ∧ ∀ (d : ℕ) (P : KoetheCounterexample.Pencil k d), ∃ (N : ℕ), 0 < N ∧ ∀ (n : ℕ), P.window v n N = 0)