Scalar Kernel Leaf Correctness

Soundness and completeness of the row-array scalar RREF kernel used by the PM-basis leaf: every emitted vector is orthogonal to the input rows, and every orthogonal vector is an F-linear combination of the emitted basis.

Scalar kernel leaf soundness

Soundness of the row-array scalar RREF kernel used by the PM-basis leaf: every vector produced by homogeneousKernelBasisRows rows cols has size cols and is orthogonal (over the first cols coordinates) to every input row.

Generic array access lemmas

theorem CompPoly.PolynomialMatrix.Approximant.array_getD_of_le' {α : Type u_2} (xs : Array α) (d : α) {i : ℕ} (h : xs.size ≤ i) : xs.getD i d = d

getD at an out-of-bounds index returns the default.

theorem CompPoly.PolynomialMatrix.Approximant.array_getD_of_lt' {α : Type u_2} (xs : Array α) (d : α) {i : ℕ} (h : i < xs.size) : xs.getD i d = xs[i]

getD at an in-bounds index returns the indexed element.

theorem CompPoly.PolynomialMatrix.Approximant.array_getD_setIfInBounds {α : Type u_2} (xs : Array α) (j : ℕ) (a : α) (i : ℕ) (d : α) : (xs.setIfInBounds j a).getD i d = if j = i ∧ j < xs.size then a else xs.getD i d

getD after setIfInBounds in coordinates.

Coordinate access helpers

theorem CompPoly.PolynomialMatrix.Approximant.addScaledScalarRow_getD {F : Type u_2} [Field F] (target source : Array F) (factor : F) (k : ℕ) : (addScaledScalarRow target source factor).getD k 0 = target.getD k 0 + factor * source.getD k 0

Coordinatewise description of addScaledScalarRow.

theorem CompPoly.PolynomialMatrix.Approximant.normalizeScalarRow_getD {F : Type u_2} [Field F] [BEq F] [LawfulBEq F] (row : Array F) (pivotCol : ℕ) (hpivot : row.getD pivotCol 0 ≠ 0) (k : ℕ) : (normalizeScalarRow row pivotCol).getD k 0 = row.getD k 0 / row.getD pivotCol 0

Coordinatewise description of normalizeScalarRow at a nonzero pivot.

Scalar dot products and orthogonality

def CompPoly.PolynomialMatrix.Approximant.scalarDot {F : Type u_2} [Field F] (cols : ℕ) (r v : Array F) : F

Dot product of the first cols coordinates of two scalar rows, with zero defaults beyond the stored lengths.

theorem CompPoly.PolynomialMatrix.Approximant.scalarDot_empty {F : Type u_2} [Field F] (cols : ℕ) (v : Array F) : scalarDot cols #[] v = 0

The empty row is orthogonal to everything.

theorem CompPoly.PolynomialMatrix.Approximant.scalarDot_addScaledScalarRow {F : Type u_2} [Field F] (cols : ℕ) (target source v : Array F) (factor : F) : scalarDot cols (addScaledScalarRow target source factor) v = scalarDot cols target v + factor * scalarDot cols source v

scalarDot is additive along addScaledScalarRow.

theorem CompPoly.PolynomialMatrix.Approximant.scalarDot_eq_pivot_mul_normalize {F : Type u_2} [Field F] [BEq F] [LawfulBEq F] (cols : ℕ) (row v : Array F) (pivotCol : ℕ) (hpivot : row.getD pivotCol 0 ≠ 0) : scalarDot cols row v = row.getD pivotCol 0 * scalarDot cols (normalizeScalarRow row pivotCol) v

A row recovers from its normalization by rescaling with the pivot.

def CompPoly.PolynomialMatrix.Approximant.OrthRows {F : Type u_2} [Field F] (cols : ℕ) (rows : Array (Array F)) (v : Array F) : Prop

Orthogonality of v to every row of a row-array matrix, expressed via total getD access so that out-of-range indices are harmless.

Elementary-step characterizations

theorem CompPoly.PolynomialMatrix.Approximant.swapScalarRows_size {F : Type u_2} (rows : Array (Array F)) (a b : ℕ) : (swapScalarRows rows a b).size = rows.size

Swapping rows preserves the row count.

Backward span: row operations are invertible

theorem CompPoly.PolynomialMatrix.Approximant.orthRows_of_scalarRrefRows {F : Type u_2} [Field F] [BEq F] [LawfulBEq F] {cols : ℕ} {rows : Array (Array F)} {v : Array F} (h : OrthRows cols (scalarRrefRows rows cols).rows v) : OrthRows cols rows v

Orthogonality to all rows of the final RREF matrix transfers back to all rows of the original matrix: every row operation is invertible.

Forward RREF shape invariants

structure CompPoly.PolynomialMatrix.Approximant.ScalarRrefSpec {F : Type u_2} [Field F] (cols : ℕ) (R : ScalarRrefResult) : Prop

Shape contract satisfied by the result of scalarRrefRows: recorded pivot columns are strictly increasing and below cols, each pivot column is a unit column with its one in the corresponding pivot row, and every row at or beyond the pivot count vanishes on all columns below cols.

• mono (s t : ℕ) : s < t → t < R.pivots.size → R.pivots.getD s 0 < R.pivots.getD t 0
• pivots_lt (t : ℕ) : t < R.pivots.size → R.pivots.getD t 0 < cols
• unit (t : ℕ) : t < R.pivots.size → ∀ (i : ℕ), (R.rows.getD i #[]).getD (R.pivots.getD t 0) 0 = if i = t then 1 else 0
• tail_zero (i : ℕ) : R.pivots.size ≤ i → ∀ k < cols, (R.rows.getD i #[]).getD k 0 = 0

theorem CompPoly.PolynomialMatrix.Approximant.scalarRrefRows_spec {F : Type u_2} [Field F] [BEq F] [LawfulBEq F] (rows : Array (Array F)) (cols : ℕ) : ScalarRrefSpec cols (scalarRrefRows rows cols)

The row-array RREF driver satisfies the RREF shape contract.

Kernel basis vectors

Main soundness theorems

theorem CompPoly.PolynomialMatrix.Approximant.homogeneousKernelBasisRows_size {F : Type u_2} [Field F] [BEq F] [LawfulBEq F] {rows : Array (Array F)} {cols : ℕ} {v : Array F} (hv : v ∈ (homogeneousKernelBasisRows rows cols).toList) : v.size = cols

Every vector produced by homogeneousKernelBasisRows rows cols has exactly cols stored coordinates.

theorem CompPoly.PolynomialMatrix.Approximant.homogeneousKernelBasisRows_dot_eq_zero {F : Type u_2} [Field F] [BEq F] [LawfulBEq F] {rows : Array (Array F)} {cols : ℕ} {v : Array F} (hv : v ∈ (homogeneousKernelBasisRows rows cols).toList) {r : Array F} (hr : r ∈ rows.toList) : ∑ k ∈ Finset.range cols, r.getD k 0 * v.getD k 0 = 0

Soundness of the scalar kernel leaf. Every vector produced by homogeneousKernelBasisRows rows cols is orthogonal, over the coordinates 0, …, cols - 1, to every row of the input matrix. No width hypothesis on the input rows is needed because the dot product only inspects the first cols coordinates (with zero defaults).

Forward span: row operations preserve orthogonality

Free-column bookkeeping for the completeness theorem

theorem CompPoly.PolynomialMatrix.Approximant.homogeneousKernelBasisRows_complete {F : Type u_2} [Field F] [BEq F] [LawfulBEq F] (rows : Array (Array F)) (cols : ℕ) {v : Array F} (hv : ∀ r ∈ rows.toList, ∑ k ∈ Finset.range cols, r.getD k 0 * v.getD k 0 = 0) (k : ℕ) : k < cols → v.getD k 0 = ∑ i ∈ Finset.range (homogeneousKernelBasisRows rows cols).size, v.getD ((DenseMatrix.freeColumns cols (scalarRrefRows rows cols).pivots).getD i 0) 0 * ((homogeneousKernelBasisRows rows cols).getD i #[]).getD k 0

Completeness of the scalar kernel leaf. Every vector orthogonal to all input rows over the coordinates 0, …, cols - 1 is, coordinatewise below cols, the F-linear combination of the emitted kernel basis vectors whose coefficients are the values of the vector at the corresponding free columns.