Kernel-Leaf Basis Generation Completeness

Every nonzero solution row of an X-adic problem lies in the row module generated by the kernel-leaf basis: the high part is generated by the monomial completion rows and the bounded remainder by the scalar kernel.

Kernel-leaf basis generation completeness

Every solution row of an X-adic problem splits into a low part, whose packed coefficient vector lies in the bounded scalar kernel, plus a high part in which every entry is divisible by X^(leafDegreeCap problem). The low part is a constant-coefficient combination of the reconstructed scalar-kernel rows by homogeneousKernelBasisRows_complete, the high part is a polynomial combination of the monomial completion rows, and the reduction and completion steps only enlarge the generated row module. Together these facts show that the kernel-leaf basis generates every solution row.

theorem CompPoly.PolynomialMatrix.Approximant.pm_append_getD_left {α : Type u_2} {A B : Array α} (d : α) {i : ℕ} (hi : i < A.size) : (A ++ B).getD i d = A.getD i d

getD of an array append, left side.

theorem CompPoly.PolynomialMatrix.Approximant.pm_append_getD_right {α : Type u_2} {A B : Array α} (d : α) {i : ℕ} (hi : A.size ≤ i) : (A ++ B).getD i d = B.getD (i - A.size) d

getD of an array append, right side.

theorem CompPoly.PolynomialMatrix.Approximant.pm_rowGet_monomialUnitRow {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (n i d k : ℕ) : rowGet (monomialUnitRow n i d) k = if k < n ∧ i = k then coeffXPower 1 d else 0

Entries of a monomial unit row.

theorem CompPoly.PolynomialMatrix.Approximant.pm_rowGet_rowLinearCombination {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (coeffs : Array (CPolynomial F)) (M : PolynomialMatrix F) (j : ℕ) : rowGet (rowLinearCombination coeffs M) j = ∑ i ∈ Finset.range (Array.size M), coeffs.getD i 0 * rowGet (Array.getD M i #[]) j

Entries of a row linear combination are coefficient-weighted entry sums.

theorem CompPoly.PolynomialMatrix.Approximant.pm_rowLinearCombination_size {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] {M : PolynomialMatrix F} {n : ℕ} (hsizes : ∀ r ∈ M.MatrixRows, Array.size r = n) (hw : M.MatrixWidth = n) (coeffs : Array (CPolynomial F)) : Array.size (rowLinearCombination coeffs M) = n

Row linear combinations of uniform-width matrices keep that width.

theorem CompPoly.PolynomialMatrix.Approximant.pm_row_ext {F : Type u_1} [Field F] {a b : PolynomialRow F} (hsize : Array.size a = Array.size b) (h : ∀ (j : ℕ), rowGet a j = rowGet b j) : a = b

Rows agreeing in size and on every rowGet entry are equal.

theorem CompPoly.PolynomialMatrix.Approximant.kernelLeafBasis_rowSpan_complete {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (mulCtx : CPolynomial.MulContext F) (problem : XAdicProblem F) (shift : Array ℕ) (hpos : 0 < Array.size problem.matrix) (hwf : problem.matrix.WellFormed) {row : PolynomialRow F} (happrox : RowApproximates mulCtx problem row) (hsize : Array.size row = Array.size problem.matrix) (_hnz : ¬RowIsZero row) : row ∈ (kernelLeafBasis problem shift).RowSpan

Generation completeness of the kernel-leaf basis. Every nonzero solution row of an X-adic problem lies in the row module generated by the kernel-leaf basis.