Shifted Weak-Popov Least-Row Minimality

Generalized predictable-degree property: any shifted weak-Popov matrix contains a row whose shifted degree is a lower bound for the shifted degree of every row-span member. This is the reducer-independent core of muldersStorjohannReduce_least_row_minimal, stated for an arbitrary well-formed shifted weak-Popov matrix and without any alignment hypothesis between the shift size and the matrix width.

theorem CompPoly.PolynomialMatrix.shiftedWeakPopov_least_row_minimal {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (B : PolynomialMatrix F) (shift : Array ℕ) (row : PolynomialRow F) (hB : B.WellFormed) (hpopov : B.ShiftedWeakPopov shift) (hrow : row ∈ B.RowSpan) (hdeg : rowShiftedDegree? row shift ≠ none) : ∃ (outRow : PolynomialRow F) (outDeg : ℕ) (rowDeg : ℕ), outRow ∈ B.MatrixRows ∧ rowShiftedDegree? outRow shift = some outDeg ∧ rowShiftedDegree? row shift = some rowDeg ∧ outDeg ≤ rowDeg

Predictable-degree property of shifted weak-Popov matrices: every row-span member with a defined shifted degree is bounded below by the shifted degree of some matrix row. Requires neither shift.size = MatrixWidth B nor any other shift alignment hypothesis.

theorem CompPoly.PolynomialMatrix.muldersStorjohannReduce_least_row_minimal_of_weakPopov {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (M : PolynomialMatrix F) (shift : Array ℕ) (row : PolynomialRow F) (hM : M.WellFormed) (hshift : shift.size = M.MatrixWidth) (hrow : row ∈ M.RowSpan) (hdeg : rowShiftedDegree? row shift ≠ none) : ∃ (outRow : PolynomialRow F) (outDeg : ℕ) (rowDeg : ℕ), outRow ∈ (M.muldersStorjohannReduce shift).MatrixRows ∧ rowShiftedDegree? outRow shift = some outDeg ∧ rowShiftedDegree? row shift = some rowDeg ∧ outDeg ≤ rowDeg

Least-row minimality of the Mulders-Storjohann reducer, re-derived from the generalized shifted weak-Popov predictable-degree property.