Documentation

CompPoly.LinearAlgebra.PolynomialMatrix.MuldersStorjohannCorrectness.Reduction

Mulders-Storjohann Correctness Reduction Invariants #

Shape, well-formedness, row-span, and weak-Popov correctness for the reducer.

source
theorem CompPoly.PolynomialMatrix.muldersStorjohannStep_shape_preserved {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] {M : PolynomialMatrix F} (shift : Array ℕ) {i j : ℕ} (hM : M.WellFormed) :
(M.muldersStorjohannStep shift i j).MatrixShape = M.MatrixShape
source
theorem CompPoly.PolynomialMatrix.muldersStorjohannStep_rowSpan_subset {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] {M : PolynomialMatrix F} (shift : Array ℕ) {i j : ℕ} (hM : M.WellFormed) :
(M.muldersStorjohannStep shift i j).RowSpan ⊆ M.RowSpan
source
theorem CompPoly.PolynomialMatrix.muldersStorjohannStep_rowSpan_superset {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] {M : PolynomialMatrix F} (shift : Array ℕ) {i j : ℕ} (hM : M.WellFormed) (hi : i < Array.size M) (hj : j < Array.size M) (hne : i ≠ j) :
M.RowSpan ⊆ (M.muldersStorjohannStep shift i j).RowSpan
source
theorem CompPoly.PolynomialMatrix.muldersStorjohannStep_wellFormed {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] {M : PolynomialMatrix F} (shift : Array ℕ) {i j : ℕ} (hM : M.WellFormed) :
(M.muldersStorjohannStep shift i j).WellFormed
source
theorem CompPoly.PolynomialMatrix.muldersStorjohannReduceWithFuel_shape_preserved {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (fuel : ℕ) (M : PolynomialMatrix F) (shift : Array ℕ) (hM : M.WellFormed) :
(muldersStorjohannReduceWithFuel fuel M shift).MatrixShape = M.MatrixShape
source
theorem CompPoly.PolynomialMatrix.muldersStorjohannReduceWithFuel_wellFormed {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (fuel : ℕ) (M : PolynomialMatrix F) (shift : Array ℕ) (hM : M.WellFormed) :
(muldersStorjohannReduceWithFuel fuel M shift).WellFormed
source
theorem CompPoly.PolynomialMatrix.muldersStorjohannReduce_wellFormed {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (M : PolynomialMatrix F) (shift : Array ℕ) (hM : M.WellFormed) :
(M.muldersStorjohannReduce shift).WellFormed
source
theorem CompPoly.PolynomialMatrix.muldersStorjohannReduceWithFuel_no_conflict_of_measure_lt {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (fuel : ℕ) (M : PolynomialMatrix F) (shift : Array ℕ) (hM : M.WellFormed) (hfuel : M.shiftedMatrixMeasure shift < fuel) :
(muldersStorjohannReduceWithFuel fuel M shift).shiftedLeadingConflict? shift = none
source
theorem CompPoly.PolynomialMatrix.muldersStorjohannReduce_no_conflict {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (M : PolynomialMatrix F) (shift : Array ℕ) (hM : M.WellFormed) :
(M.muldersStorjohannReduce shift).shiftedLeadingConflict? shift = none
source
theorem CompPoly.PolynomialMatrix.muldersStorjohannReduceWithFuel_eq_of_no_conflict {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (f g : ℕ) (M : PolynomialMatrix F) (shift : Array ℕ) :
(muldersStorjohannReduceWithFuel f M shift).shiftedLeadingConflict? shift = none → (muldersStorjohannReduceWithFuel g M shift).shiftedLeadingConflict? shift = none → muldersStorjohannReduceWithFuel f M shift = muldersStorjohannReduceWithFuel g M shift

The fueled reducer is deterministic: two runs that both end without a shifted leading conflict stopped at the same (first conflict-free) matrix of the common step orbit, regardless of their fuel.

source
theorem CompPoly.PolynomialMatrix.muldersStorjohannReduceWithFuel_rowSpan_subset {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (fuel : ℕ) (M : PolynomialMatrix F) (shift : Array ℕ) (hM : M.WellFormed) :
(muldersStorjohannReduceWithFuel fuel M shift).RowSpan ⊆ M.RowSpan
source
theorem CompPoly.PolynomialMatrix.muldersStorjohannReduce_rowSpan_subset {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (M : PolynomialMatrix F) (shift : Array ℕ) (hM : M.WellFormed) :
(M.muldersStorjohannReduce shift).RowSpan ⊆ M.RowSpan
source
theorem CompPoly.PolynomialMatrix.muldersStorjohannReduceWithFuel_rowSpan_superset {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (fuel : ℕ) (M : PolynomialMatrix F) (shift : Array ℕ) (hM : M.WellFormed) :
M.RowSpan ⊆ (muldersStorjohannReduceWithFuel fuel M shift).RowSpan
source
theorem CompPoly.PolynomialMatrix.muldersStorjohannReduce_rowSpan_superset {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (M : PolynomialMatrix F) (shift : Array ℕ) (hM : M.WellFormed) :
M.RowSpan ⊆ (M.muldersStorjohannReduce shift).RowSpan
source
theorem CompPoly.PolynomialMatrix.muldersStorjohannReduce_shape_preserved {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (M : PolynomialMatrix F) (shift : Array ℕ) (hM : M.WellFormed) :
(M.muldersStorjohannReduce shift).MatrixShape = M.MatrixShape
source
theorem CompPoly.PolynomialMatrix.muldersStorjohannReduce_rowSpan_eq {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (M : PolynomialMatrix F) (shift : Array ℕ) (hM : M.WellFormed) :
(M.muldersStorjohannReduce shift).RowSpan = M.RowSpan
source
theorem CompPoly.PolynomialMatrix.muldersStorjohannReduce_weakPopov {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (M : PolynomialMatrix F) (shift : Array ℕ) (hM : M.WellFormed) (_hshift : shift.size = M.MatrixWidth) :
(M.muldersStorjohannReduce shift).ShiftedWeakPopov shift