Kernel-Leaf Basis Soundness

Every row of the kernel-leaf basis satisfies the X-adic approximant conditions and has the principal row width: kernel vectors reconstruct to solutions, and the reduction, completion, and compaction steps preserve soundness.

Kernel-leaf basis soundness

theorem CompPoly.PolynomialMatrix.Approximant.rowScaleCoeffX_size {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (c : F) (d : ℕ) (row : PolynomialRow F) : Array.size (rowScaleCoeffX c d row) = Array.size row

Coefficient-shift row scaling preserves the row size.

theorem CompPoly.PolynomialMatrix.Approximant.pivotRows_invariant {F : Type u_1} [Field F] (Q : PolynomialRow F → Prop) {pivots : Array (Option (PolynomialRow F))} (hpivots : ∀ (p : ℕ) (r : PolynomialRow F), pivots.getD p none = some r → Q r) {row : PolynomialRow F} (hrow : row ∈ (pivotRows pivots).MatrixRows) : Q row

Any predicate holding for all stored pivot rows holds for all extracted rows.

theorem CompPoly.PolynomialMatrix.Approximant.reduceKernelLeafRowsByPivots_invariant {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (Q : PolynomialRow F → Prop) (hclosed : ∀ (target reducer : PolynomialRow F) (shift : Array ℕ), Q target → Q reducer → Q (cancelKernelLeafLeadingTerm target reducer shift)) {rows : PolynomialMatrix F} (shift : Array ℕ) (hrows : ∀ row ∈ rows.MatrixRows, Q row) {row : PolynomialRow F} (hrow : row ∈ (reduceKernelLeafRowsByPivots rows shift).MatrixRows) : Q row

Any predicate closed under leading-term cancellation is preserved by the pivot-table reduction.

theorem CompPoly.PolynomialMatrix.Approximant.mem_matrixRows_push {F : Type u_1} [Field F] {rows : PolynomialMatrix F} {row r : PolynomialRow F} (hr : r ∈ MatrixRows (Array.push rows row)) : r ∈ rows.MatrixRows ∨ r = row

A row of rows.push row is either a row of rows or row itself.

theorem CompPoly.PolynomialMatrix.Approximant.reduceKernelLeafRowsIncremental_invariant {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (Q : PolynomialRow F → Prop) (hclosed : ∀ (target reducer : PolynomialRow F) (shift : Array ℕ), Q target → Q reducer → Q (cancelKernelLeafLeadingTerm target reducer shift)) {rows : PolynomialMatrix F} (shift : Array ℕ) (hrows : ∀ row ∈ rows.MatrixRows, Q row) {row : PolynomialRow F} (hrow : row ∈ (reduceKernelLeafRowsIncremental rows shift).MatrixRows) : Q row

Any predicate closed under leading-term cancellation is preserved by the incremental pivot reduction.

theorem CompPoly.PolynomialMatrix.Approximant.rowGet_vectorToPolynomialRow_coeff {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (cap width : ℕ) (v : Array F) (k a : ℕ) : (rowGet (vectorToPolynomialRow cap width v) k).coeff a = if k < width ∧ a < cap then v.getD (k * cap + a) 0 else 0

Coefficients of polynomial rows reconstructed from scalar vectors.

theorem CompPoly.PolynomialMatrix.Approximant.vectorToPolynomialRow_approximates {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (mulCtx : CPolynomial.MulContext F) (problem : XAdicProblem F) {v : Array F} (hv : v ∈ (homogeneousKernelBasisRows (coefficientMatrixRows problem) (Array.size problem.matrix * leafDegreeCap problem)).toList) : RowApproximates mulCtx problem (vectorToPolynomialRow (leafDegreeCap problem) (Array.size problem.matrix) v)

Polynomial rows reconstructed from scalar kernel vectors satisfy the X-adic conditions of the bounded leaf problem.

theorem CompPoly.PolynomialMatrix.Approximant.pm_pack_index {cap : ℕ} (hcap : 0 < cap) {size k a : ℕ} (hk : k < size) (ha : a < cap) : k * cap + a < size * cap ∧ (k * cap + a) / cap = k ∧ (k * cap + a) % cap = a

Arithmetic of the packed index k * cap + a.

def CompPoly.PolynomialMatrix.Approximant.rowToCoefficientVector {F : Type u_1} [Field F] (problem : XAdicProblem F) (row : PolynomialRow F) : Array F

Pack the coefficients below the leaf degree cap of a polynomial row into one flat scalar vector: coefficient a of coordinate k is stored at index k * leafDegreeCap problem + a. This is the coefficient-side inverse of vectorToPolynomialRow.

theorem CompPoly.PolynomialMatrix.Approximant.vectorToPolynomialRow_rowToCoefficientVector {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (problem : XAdicProblem F) {row : PolynomialRow F} (hsize : Array.size row = Array.size problem.matrix) (hdeg : ∀ k < Array.size row, ∀ (a : ℕ), leafDegreeCap problem ≤ a → (rowGet row k).coeff a = 0) : vectorToPolynomialRow (leafDegreeCap problem) (Array.size problem.matrix) (rowToCoefficientVector problem row) = row

Reconstructing a polynomial row from its packed coefficient vector is the identity on rows of the principal width whose coefficients respect the leaf degree cap.

theorem CompPoly.PolynomialMatrix.Approximant.coefficientMatrixRows_dot_eq_zero_of_approximates {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (mulCtx : CPolynomial.MulContext F) (problem : XAdicProblem F) {row : PolynomialRow F} (happrox : RowApproximates mulCtx problem row) (hwf : problem.matrix.WellFormed) (r : Array F) : r ∈ (coefficientMatrixRows problem).toList → ∑ c ∈ Finset.range (Array.size problem.matrix * leafDegreeCap problem), r.getD c 0 * (rowToCoefficientVector problem row).getD c 0 = 0

Converse coefficient bridge. A polynomial row of a well-formed bounded leaf problem that satisfies the X-adic conditions yields a packed coefficient vector orthogonal to every scalar coefficient row.

theorem CompPoly.PolynomialMatrix.Approximant.kernelLeafBasis_rows {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (mulCtx : CPolynomial.MulContext F) (problem : XAdicProblem F) (shift : Array ℕ) (row : PolynomialRow F) : row ∈ (kernelLeafBasis problem shift).MatrixRows → RowApproximates mulCtx problem row ∧ Array.size row = Array.size problem.matrix

Every kernel-leaf basis row approximates the problem and has the principal row width.