Root-row pencils and the polynomial root-column argument

A finite homogeneous-linear system becomes a shared Pencil by multiplying its output row by the central polynomial variable. If that matrix is nilpotent, 1 - T has a polynomial right inverse. Eliminating the internal entries of its root column gives q = 1 + X * C(x) * q. The coefficients of this polynomial are x^n, and their eventual vanishing proves nilpotence of x.

theorem KoetheCounterexample.Linearization.nilpotent_of_polynomial_resolvent {R : Type v} [Ring R] (x : R) (q : Polynomial R) (hq : q = 1 + Polynomial.X * (Polynomial.C x * q)) : IsNilpotent x

A polynomial right resolvent forces nilpotence, also in a noncommutative ring and without assuming that the ring is nontrivial.

def KoetheCounterexample.Linearization.submatrixHom {ι : Type u_1} {κ : Type u_2} {A : Type u_3} [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ] [Semiring A] (e : ι ≃ κ) : Matrix κ κ A →*₀ Matrix ι ι A

Reindexing square matrices preserves products, zero, and one.

Equations

• KoetheCounterexample.Linearization.submatrixHom e = { toFun := fun (M : Matrix κ κ A) => M.submatrix ⇑e ⇑e, map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯ }

noncomputable def KoetheCounterexample.Linearization.System.matrix {k : Type u} [Field k] {R : Type v} [Ring R] [Algebra k R] (S : System k) (a : Fin 3 → R) : Matrix (Option S.State) (Option S.State) (Polynomial R)

The root is none; only its row contains X.

Equations

• S.matrix a none none = Polynomial.X * KoetheCounterexample.Linearization.edge a S.head
• S.matrix a none (some j_2) = Polynomial.X * KoetheCounterexample.Linearization.edge a (S.out j_2)
• S.matrix a (some i_2) none = KoetheCounterexample.Linearization.edge a (S.input i_2)
• S.matrix a (some i_2) (some j_2) = KoetheCounterexample.Linearization.edge a (S.step i_2 j_2)

noncomputable def KoetheCounterexample.Linearization.System.indexEquiv {k : Type u} [Field k] (S : System k) : Fin (Fintype.card S.State + 1) ≃ Option S.State

Enumeration of the states with the shared root index 0.

Equations

• S.indexEquiv = (finSuccEquiv (Fintype.card S.State)).trans (Fintype.equivFin S.State).symm.optionCongr

@[simp]

theorem KoetheCounterexample.Linearization.System.indexEquiv_zero {k : Type u} [Field k] (S : System k) : S.indexEquiv 0 = none

noncomputable def KoetheCounterexample.Linearization.System.pencil {k : Type u} [Field k] (S : System k) : Pencil k (Fintype.card S.State)

Exactly the shared pencil API, with no scalar/identity edges.

Equations

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

theorem KoetheCounterexample.Linearization.System.lift_pencil {k : Type u} [Field k] {R : Type v} [Ring R] [Algebra k R] (S : System k) (a : Fin 3 → R) : S.pencil.lift a = (S.matrix a).submatrix ⇑S.indexEquiv ⇑S.indexEquiv

Evaluation agrees with the system matrix, including the exact order of scalar coefficients, generator factors, and the central variable.

theorem KoetheCounterexample.Linearization.System.matrix_nil_of_pencil_nil {k : Type u} [Field k] {R : Type v} [Ring R] [Algebra k R] (S : System k) (a : Fin 3 → R) (h : IsNilpotent (S.pencil.lift a)) : IsNilpotent (S.matrix a)

Nilpotence transfers from the shared, finitely indexed pencil to the same matrix indexed by the root and internal states.

theorem KoetheCounterexample.Linearization.Represents.nil_of_matrix_nil {k : Type u} [Field k] {R : Type v} [Ring R] [Algebra k R] {S : System k} {a : Fin 3 → R} {x : R} (hS : Represents S a x) (hT : IsNilpotent (S.matrix a)) : IsNilpotent x

Eliminate the internal entries of the root column of a polynomial right inverse. Nilpotence is only used to obtain this right inverse.

theorem KoetheCounterexample.Linearization.Represents.nil_of_pencil_nil {k : Type u} [Field k] {R : Type v} [Ring R] [Algebra k R] {S : System k} {a : Fin 3 → R} {x : R} (hS : Represents S a x) (hT : IsNilpotent (S.pencil.lift a)) : IsNilpotent x

Each finite linearization gives a single-row pencil whose nilpotence implies nilpotence of the represented element.