Kernel-Leaf Reduction Row-Span Soundness

The shifted pivot-table reduction preserves the generated row module: the fuel bound dominates the shifted row measure, every displaced row re-enters the table as a reduced combination, and the incremental reduction loop keeps every input row inside the span of its output.

Kernel-leaf reduction row-span soundness

The pivot-table reduction only ever replaces rows by row operations that are invertible inside the generated row module, so no original row leaves the row span. The proofs below make this precise: leading-term cancellation is the Mulders-Storjohann cancellation in disguise, the pivot-table insertion loop is tracked through a fuel-indexed measure argument, and the incremental reducer chains the per-call result through row-span transitivity.

theorem CompPoly.PolynomialMatrix.Approximant.rowIsZero_eq_zeroRow {F : Type u_1} [Field F] [BEq F] {row : PolynomialRow F} (h : RowIsZero row) : row = zeroRow (Array.size row)

A zero row is the zero row of its width.

theorem CompPoly.PolynomialMatrix.Approximant.size_pos_of_mem_matrixRows {F : Type u_1} [Field F] {M : PolynomialMatrix F} {r : PolynomialRow F} (h : r ∈ M.MatrixRows) : 0 < Array.size M

Matrices with a member row are nonempty.

theorem CompPoly.PolynomialMatrix.Approximant.wellFormed_of_sizes {F : Type u_1} [Field F] {M : PolynomialMatrix F} {n : ℕ} (h : ∀ r ∈ M.MatrixRows, Array.size r = n) : M.WellFormed

Uniform row widths make a matrix well formed.

theorem CompPoly.PolynomialMatrix.Approximant.eq_empty_of_mem_rowSpan_empty {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] {x : PolynomialRow F} (hx : x ∈ RowSpan #[]) : x = #[]

The row span of the empty matrix only contains the empty row.

theorem CompPoly.PolynomialMatrix.Approximant.insertKernelLeaf_foldl_pivotInv {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] {n : ℕ} (l : List (PolynomialRow F)) (fuel : ℕ) (pivots : Array (Option (PolynomialRow F))) (shift : Array ℕ) : (∀ r ∈ l, Array.size r = n) → (∀ (p : ℕ) (r : PolynomialRow F), pivots.getD p none = some r → Array.size r = n ∧ rowShiftedLeadingPosition? r shift = some p) → ∀ (p : ℕ) (r : PolynomialRow F), (List.foldl (fun (pv : Array (Option (PolynomialRow F))) (r : PolynomialRow F) => insertKernelLeafPivotRowWithFuel fuel pv shift r) pivots l).getD p none = some r → Array.size r = n ∧ rowShiftedLeadingPosition? r shift = some p

Folded pivot-table insertion preserves the table invariant.

theorem CompPoly.PolynomialMatrix.Approximant.reduceKernelLeafRowsByPivots_rowSpan_superset {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] {rows : PolynomialMatrix F} {shift : Array ℕ} {n : ℕ} (hsizes : ∀ r ∈ rows.MatrixRows, Array.size r = n) {row : PolynomialRow F} (hrow : row ∈ rows.MatrixRows) (hnz : ¬RowIsZero row) : row ∈ (reduceKernelLeafRowsByPivots rows shift).RowSpan

The pivot-table reduction preserves the generated row module: every nonzero source row stays inside the row span of the reduced matrix.

theorem CompPoly.PolynomialMatrix.Approximant.reduceKernelLeafRowsByPivots_rows {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] {n : ℕ} {rows : PolynomialMatrix F} {shift : Array ℕ} (hsizes : ∀ r ∈ rows.MatrixRows, Array.size r = n) (r : PolynomialRow F) : r ∈ (reduceKernelLeafRowsByPivots rows shift).MatrixRows → Array.size r = n ∧ rowIsZero r = false

Reduced kernel-leaf rows keep the uniform width and are nonzero.

theorem CompPoly.PolynomialMatrix.Approximant.rowIsZero_empty {F : Type u_1} [Field F] [BEq F] : RowIsZero #[]

The empty row is a zero row.

theorem CompPoly.PolynomialMatrix.Approximant.reduceKernelLeafRowsIncremental_rowSpan_superset {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] {rows : PolynomialMatrix F} {shift : Array ℕ} {n : ℕ} (hsizes : ∀ r ∈ rows.MatrixRows, Array.size r = n) {row : PolynomialRow F} (hrow : row ∈ rows.MatrixRows) (hnz : ¬RowIsZero row) : row ∈ (reduceKernelLeafRowsIncremental rows shift).RowSpan

The incremental kernel-leaf reduction preserves the generated row module: every nonzero source row stays inside the row span of the reduced basis.