Fast Mulders-Storjohann Reduction Agrees With the Direct Definition

The fast reducer caches shifted leading positions once per conflict scan and cancels leading terms through the fused rowSubScaledShift update. This file proves it extensionally equal to muldersStorjohannReduce, so every correctness result transfers, and packages it as a certified ShiftedRowReducerContext.

Row-level cancellation

theorem CompPoly.PolynomialMatrix.rowSubScaledShift_size {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (a : PolynomialRow F) (c : F) (d : ℕ) (b : PolynomialRow F) : Array.size (rowSubScaledShift a c d b) = max (Array.size a) (Array.size b)

theorem CompPoly.PolynomialMatrix.rowGet_rowSubScaledShift {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (a : PolynomialRow F) (c : F) (d : ℕ) (b : PolynomialRow F) (j : ℕ) : rowGet (rowSubScaledShift a c d b) j = (rowGet a j).subMulMonomial c d (rowGet b j)

theorem CompPoly.PolynomialMatrix.rowSubScaledShift_eq {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (a : PolynomialRow F) (c : F) (d : ℕ) (b : PolynomialRow F) : rowSubScaledShift a c d b = rowSub a (rowScaleMonomial c d b)

theorem CompPoly.PolynomialMatrix.cancelShiftedLeadingTermFast_eq {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (target reducer : PolynomialRow F) (shift : Array ℕ) : cancelShiftedLeadingTermFast target reducer shift = cancelShiftedLeadingTerm target reducer shift

Cached conflict scan

theorem CompPoly.PolynomialMatrix.rowLeadingPositions_size {F : Type u_1} [Field F] [BEq F] (M : PolynomialMatrix F) (shift : Array ℕ) : (M.rowLeadingPositions shift).size = Array.size M

theorem CompPoly.PolynomialMatrix.rowLeadingPositions_getD {F : Type u_1} [Field F] [BEq F] (M : PolynomialMatrix F) (shift : Array ℕ) {i : ℕ} (hi : i < Array.size M) : (M.rowLeadingPositions shift).getD i none = rowShiftedLeadingPosition? (Array.getD M i #[]) shift

theorem CompPoly.PolynomialMatrix.cachedLeadingConflictInRowStep?_eq {F : Type u_1} [Field F] [BEq F] (M : PolynomialMatrix F) (shift : Array ℕ) {i j : ℕ} (hi : i < Array.size M) (hj : j < Array.size M) (found : Option (ℕ × ℕ)) : cachedLeadingConflictInRowStep? (M.rowLeadingPositions shift) i found j = M.shiftedLeadingConflictInRowStep? shift i found j

theorem CompPoly.PolynomialMatrix.cachedLeadingConflictInRow?_eq {F : Type u_1} [Field F] [BEq F] (M : PolynomialMatrix F) (shift : Array ℕ) {i : ℕ} (hi : i < Array.size M) (found : Option (ℕ × ℕ)) : cachedLeadingConflictInRow? (M.rowLeadingPositions shift) i found = M.shiftedLeadingConflictInRow? shift i found

theorem CompPoly.PolynomialMatrix.cachedLeadingConflict?_eq {F : Type u_1} [Field F] [BEq F] (M : PolynomialMatrix F) (shift : Array ℕ) : cachedLeadingConflict? (M.rowLeadingPositions shift) = M.shiftedLeadingConflict? shift

Step, loop, and reducer

theorem CompPoly.PolynomialMatrix.muldersStorjohannStepFast_eq {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (M : PolynomialMatrix F) (shift : Array ℕ) (i j : ℕ) : M.muldersStorjohannStepFast shift i j = M.muldersStorjohannStep shift i j

theorem CompPoly.PolynomialMatrix.muldersStorjohannReduceWithFuelFast_eq {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (fuel : ℕ) (M : PolynomialMatrix F) (shift : Array ℕ) : muldersStorjohannReduceWithFuelFast fuel M shift = muldersStorjohannReduceWithFuel fuel M shift

theorem CompPoly.PolynomialMatrix.muldersStorjohannReduceFast_eq {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (M : PolynomialMatrix F) (shift : Array ℕ) : M.muldersStorjohannReduceFast shift = M.muldersStorjohannReduce shift

Certified context

def CompPoly.PolynomialMatrix.muldersStorjohannFastReducerContext (F : Type u_2) [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] : ShiftedRowReducerContext F

Certified fast Mulders-Storjohann shifted row-reducer context. The implementation caches leading positions per scan and uses fused row cancellation; correctness transfers along muldersStorjohannReduceFast_eq.