Recursive PM-Basis Correctness

Soundness and shifted minimality of the kernel-leaf recursive PM-basis: every produced row satisfies the X-adic conditions with the principal width, the recursion generates the full solution module, and the root-normalized basis is shifted weak Popov, so the predictable-degree property yields a basis row dominating every nonzero solution.

theorem CompPoly.PolynomialMatrix.Approximant.pmBasisWithFuelCore_kernelLeaf_rows {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (mulCtx : CPolynomial.MulContext F) (lowCtx : MulLowContext F) (leafCutoff composeLeafCutoff fuel : ℕ) (problem : XAdicProblem F) (shift : Array ℕ) (row : PolynomialRow F) : row ∈ (pmBasisWithFuelCore (kernelLeafRuntimeWithLowAndCompose mulCtx lowCtx leafCutoff composeLeafCutoff) fuel problem shift).MatrixRows → RowApproximates mulCtx problem row ∧ Array.size row = Array.size problem.matrix

Every row of the fuel-bounded kernel-leaf PM-basis core approximates the problem and has the principal row width.

theorem CompPoly.PolynomialMatrix.Approximant.pmBasis_kernelLeaf_approximates {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (mulCtx : CPolynomial.MulContext F) (lowCtx : MulLowContext F) (leafCutoff composeLeafCutoff : ℕ) (problem : XAdicProblem F) (shift : Array ℕ) {row : PolynomialRow F} (hrow : row ∈ (pmBasis (kernelLeafRuntimeWithLowAndCompose mulCtx lowCtx leafCutoff composeLeafCutoff) problem shift).MatrixRows) : RowApproximates mulCtx problem row

Every row of the kernel-leaf recursive PM-basis satisfies the X-adic approximant conditions.

Generation completeness of the recursive PM-basis core

Every nonzero solution row of an X-adic problem lies in the row module generated by the recursive PM-basis core. Together with the shifted weak-Popov shape of the root normalization this yields the predictable-degree minimality of the final basis.

theorem CompPoly.PolynomialMatrix.Approximant.pmBasisWithFuelCore_kernelLeaf_rowSpan_complete {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (mulCtx : CPolynomial.MulContext F) (lowCtx : MulLowContext F) (leafCutoff composeLeafCutoff fuel : ℕ) (problem : XAdicProblem F) (shift : Array ℕ) : 0 < Array.size problem.matrix → problem.matrix.WellFormed → ∀ (row : PolynomialRow F), RowApproximates mulCtx problem row → Array.size row = Array.size problem.matrix → ¬RowIsZero row → row ∈ (pmBasisWithFuelCore (kernelLeafRuntimeWithLowAndCompose mulCtx lowCtx leafCutoff composeLeafCutoff) fuel problem shift).RowSpan

Generation completeness of the recursive PM-basis core. Every nonzero solution row of an X-adic problem lies in the row module generated by the fuel-bounded recursive PM-basis core.

Root normalization shape and shifted minimality

theorem CompPoly.PolynomialMatrix.Approximant.pmBasis_kernelLeaf_complete_minimal {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (mulCtx : CPolynomial.MulContext F) (lowCtx : MulLowContext F) (leafCutoff composeLeafCutoff : ℕ) (problem : XAdicProblem F) (shift : Array ℕ) (row : PolynomialRow F) (hpos : 0 < Array.size problem.matrix) (hwf : problem.matrix.WellFormed) (happrox : RowApproximates mulCtx problem row) (hnz : rowIsZero row = false) (hwidth : Array.size row ≤ Array.size problem.matrix) : ∃ (basisRow : PolynomialRow F) (degree : ℕ), basisRow ∈ (pmBasis (kernelLeafRuntimeWithLowAndCompose mulCtx lowCtx leafCutoff composeLeafCutoff) problem shift).MatrixRows ∧ Array.size basisRow ≤ Array.size problem.matrix ∧ rowShiftedDegree? basisRow shift = some degree ∧ ∀ (rowDegree : ℕ), rowShiftedDegree? row shift = some rowDegree → degree ≤ rowDegree

Shifted minimality of the recursive PM-basis. Every nonzero X-adic solution row is shifted-degree dominated by some row of the root-normalized recursive PM-basis.