Mask mortality for one-row pencils over an algebraically closed field

The proof uses determinantal rank: vanishing (r+1)-minors is the rank bound, and one nonzero r-minor is a pivot. A long connector kills that pivot in P_W P_C P_W, so all r-minors vanish. Induction finishes in at most the matrix size many strict rank reductions.

Every connector hole is independently enumerated, all chosen vectors lie in the constant field, and all products are in the forward word convention of KoethePencilDefs. No nilness or countability hypothesis is used.

theorem KoetheCounterexample.Mortality.exists_rank_reducing_connector {k : Type u_1} [Field k] [IsAlgClosed k] {d r : ℕ} (P : Pencil k d) (M : PeriodicMask k) (hM : M.period < 2 * M.holes) (w : List (Triple k)) (hr : 0 < r) (I J : Fin r → Fin (d + 1)) (hp : ((P.wordProd w).submatrix I J).det ≠ 0) (hnext : MinorsVanish (P.wordProd w) (r + 1)) : ∃ (c : List (Triple k)), M.period ≤ c.length ∧ M.period ∣ c.length ∧ (∀ z ∈ c, z ≠ 0) ∧ M.Compatible c ∧ MinorsVanish (P.wordProd (w ++ c ++ w)) r

A sufficiently long, mask-compatible connector strictly reduces a positive determinantal rank.

theorem KoetheCounterexample.Mortality.mortality_of_vanishing_minors {k : Type u_1} [Field k] [IsAlgClosed k] {d : ℕ} (P : Pencil k d) (M : PeriodicMask k) (hM : M.period < 2 * M.holes) (r : ℕ) (w : List (Triple k)) : M.period ≤ w.length → M.period ∣ w.length → (∀ z ∈ w, z ≠ 0) → M.Compatible w → MinorsVanish (P.wordProd w) (r + 1) → ∃ (u : List (Triple k)), M.period ≤ u.length ∧ M.period ∣ u.length ∧ (∀ z ∈ u, z ≠ 0) ∧ M.Compatible u ∧ P.wordProd u = 0

Induction on a determinantal rank bound, retaining a positive, aligned, mask-compatible nonzero word throughout.

theorem KoetheCounterexample.maskMortality (k : Type u_1) [Field k] [IsAlgClosed k] : MaskMortality k

Mask mortality. A periodic mask with more than half of its residues free admits a compatible nonzero mortal word for every one-row pencil over an algebraically closed field.