Nilness of the positive algebra from nilness of all root-row pencils

Every element of the nonunital algebra generated by three elements admits a finite homogeneous-linear system. Its root-row pencil belongs to the exact shared Pencil type, and nilpotence of that pencil implies nilpotence of the element.

The strengthened adjoin induction below proves multiplication closure without adding scalar/identity edges: besides linearizing x, it proves that left multiplication by x preserves linearizability. At a generator this is the prepend construction; the multiplication step is then composition.

theorem KoetheCounterexample.Linearization.linearizable_of_mem_adjoin {k : Type u} [Field k] {R : Type v} [Ring R] [Algebra k R] (a : Fin 3 → R) {x : R} (hx : x ∈ NonUnitalAlgebra.adjoin k (Set.range a)) : Linearizable a x

Every positive algebra expression admits a finite homogeneous-linear system. No dimension, cardinality, commutativity, or nilness hypothesis on the ambient algebra is needed.

theorem KoetheCounterexample.exists_pencil_nil_imp_of_mem_adjoin {k : Type u} [Field k] {R : Type v} [Ring R] [Algebra k R] (a : Fin 3 → R) {x : R} (hx : x ∈ NonUnitalAlgebra.adjoin k (Set.range a)) : ∃ (d : ℕ) (P : Pencil k d), IsNilpotent (P.lift a) → IsNilpotent x

A per-element root-row pencil certificate for any element of the generated positive algebra. Its entries are homogeneous-linear in the generators, and its parameter occurs solely in the distinguished row.

theorem KoetheCounterexample.nil_of_all_pencils_nil {k : Type u} [Field k] {R : Type v} [Ring R] [Algebra k R] (a : Fin 3 → R) (hall : ∀ (d : ℕ) (P : Pencil k d), IsNilpotent (P.lift a)) (x : R) : x ∈ NonUnitalAlgebra.adjoin k (Set.range a) → IsNilpotent x

If all homogeneous-linear, single-root-row pencils in the three generators are nilpotent, then their generated nonunital algebra is nil.