The one-row parameter-degree bound

Multilinearity in the rows expands a minor of a product into row products of the first factor and minors of the remaining factors. Repeated rows make the latter minors zero. Thus a single parameter row contributes at most one to the degree per factor, not the size of the minor.

theorem KoetheCounterexample.Mortality.lift_entry_natDegree_le {k : Type u_1} {R : Type u_2} [Field k] [CommRing R] [Algebra k R] {d : ℕ} (P : Pencil k d) (a : Fin 3 → R) (i j : Fin (d + 1)) : (P.lift a i j).natDegree ≤ 1

theorem KoetheCounterexample.Mortality.lift_entry_natDegree_off_root {k : Type u_1} {R : Type u_2} [Field k] [CommRing R] [Algebra k R] {d : ℕ} (P : Pencil k d) (a : Fin 3 → R) (i j : Fin (d + 1)) (hi : i ≠ 0) : (P.lift a i j).natDegree = 0

theorem KoetheCounterexample.Mortality.lift_row_prod_natDegree_le {k : Type u_1} {R : Type u_2} [Field k] [CommRing R] [Algebra k R] {d r : ℕ} (P : Pencil k d) (a : Fin 3 → R) (I f : Fin r → Fin (d + 1)) (hI : Function.Injective I) : (∏ i : Fin r, P.lift a (I i) (f i)).natDegree ≤ 1

A product using distinct rows of one factor has parameter degree at most one.

theorem KoetheCounterexample.Mortality.det_liftWord_natDegree_le {k : Type u_1} {R : Type u_2} [Field k] [CommRing R] [Algebra k R] {d r : ℕ} (P : Pencil k d) (w : List (Fin 3 → R)) (I J : Fin r → Fin (d + 1)) (hI : Function.Injective I) : ((List.map P.lift w).prod.submatrix I J).det.natDegree ≤ w.length

Every minor of a forward word of lifted letters has degree at most the word length. The coefficient ring is an arbitrary commutative k-algebra.