X-Adic Row Soundness Toolkit

The RowApproximates predicate, its divisibility characterization, closure under the row operations used by the leaf reduction and completion steps, and the soundness of one divide-and-conquer composition step.

X-adic row soundness toolkit

Semantic tools for proving that every row produced by the recursive PM-basis driver satisfies the X-adic approximant conditions. Soundness is phrased via X^order divisibility of the toPoly image, which makes it closed under the row operations used by the reduction, completion, and composition steps.

def CompPoly.PolynomialMatrix.Approximant.RowApproximates {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (mulCtx : CPolynomial.MulContext F) (problem : XAdicProblem F) (row : PolynomialRow F) : Prop

A row approximates an X-adic problem when every column product vanishes to the required order.

theorem CompPoly.PolynomialMatrix.Approximant.truncateX_eq_zero_iff_X_pow_dvd {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (order : ℕ) (p : CPolynomial F) : truncateX order p = 0 ↔ Polynomial.X ^ order ∣ p.toPoly

Truncation vanishes exactly on X^order-multiples under toPoly.

theorem CompPoly.PolynomialMatrix.Approximant.truncateX_zero_eq_zero {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (order : ℕ) : truncateX order 0 = 0

Truncation of the zero polynomial is zero.

theorem CompPoly.PolynomialMatrix.Approximant.pm_toPoly_finset_sum {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (f : ℕ → CPolynomial F) (n : ℕ) : (∑ k ∈ Finset.range n, f k).toPoly = ∑ k ∈ Finset.range n, (f k).toPoly

toPoly commutes with finite range sums.

theorem CompPoly.PolynomialMatrix.Approximant.rowGet_rowMulMatrixWith_toPoly {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (mulCtx : CPolynomial.MulContext F) (row : PolynomialRow F) (M : PolynomialMatrix F) {j : ℕ} (hj : j < M.MatrixWidth) : (rowGet (rowMulMatrixWith mulCtx row M) j).toPoly = ∑ k ∈ Finset.range (Array.size M), (rowGet row k).toPoly * (rowGet (Array.getD M k #[]) j).toPoly

Column entries of a row-by-matrix product as sums over the matrix height, under toPoly.

theorem CompPoly.PolynomialMatrix.Approximant.rowApproximates_iff {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (mulCtx : CPolynomial.MulContext F) (problem : XAdicProblem F) (row : PolynomialRow F) : RowApproximates mulCtx problem row ↔ ∀ j < problem.orders.size, j < problem.matrix.MatrixWidth → Polynomial.X ^ problem.orders.getD j 0 ∣ ∑ k ∈ Finset.range (Array.size problem.matrix), (rowGet row k).toPoly * (rowGet (Array.getD problem.matrix k #[]) j).toPoly

Divisibility form of the approximant condition, one column at a time.

theorem CompPoly.PolynomialMatrix.Approximant.rowApproximates_rowSub {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (mulCtx : CPolynomial.MulContext F) (problem : XAdicProblem F) {a b : PolynomialRow F} (ha : RowApproximates mulCtx problem a) (hb : RowApproximates mulCtx problem b) : RowApproximates mulCtx problem (rowSub a b)

Row subtraction preserves the approximant condition.

theorem CompPoly.PolynomialMatrix.Approximant.polynomialScaleCoeffX_toPoly {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (c : F) (d : ℕ) (p : CPolynomial F) : (polynomialScaleCoeffX c d p).toPoly = Polynomial.C c * Polynomial.X ^ d * p.toPoly

Coefficient-shift scaling under toPoly.

theorem CompPoly.PolynomialMatrix.Approximant.rowApproximates_rowScaleCoeffX {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (mulCtx : CPolynomial.MulContext F) (problem : XAdicProblem F) {row : PolynomialRow F} (c : F) (d : ℕ) (h : RowApproximates mulCtx problem row) : RowApproximates mulCtx problem (rowScaleCoeffX c d row)

Coefficient-shift row scaling preserves the approximant condition.

theorem CompPoly.PolynomialMatrix.Approximant.rowApproximates_cancelKernelLeafLeadingTerm {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (mulCtx : CPolynomial.MulContext F) (problem : XAdicProblem F) {target reducer : PolynomialRow F} (shift : Array ℕ) (htarget : RowApproximates mulCtx problem target) (hreducer : RowApproximates mulCtx problem reducer) : RowApproximates mulCtx problem (cancelKernelLeafLeadingTerm target reducer shift)

Leading-term cancellation preserves the approximant condition.

theorem CompPoly.PolynomialMatrix.Approximant.insertKernelLeafPivotRowWithFuel_approximates {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (mulCtx : CPolynomial.MulContext F) (problem : XAdicProblem F) (fuel : ℕ) (pivots : Array (Option (PolynomialRow F))) (shift : Array ℕ) (row : PolynomialRow F) : (∀ (p : ℕ) (r : PolynomialRow F), pivots.getD p none = some r → RowApproximates mulCtx problem r) → RowApproximates mulCtx problem row → ∀ (p : ℕ) (r : PolynomialRow F), (insertKernelLeafPivotRowWithFuel fuel pivots shift row).getD p none = some r → RowApproximates mulCtx problem r

Pivot-table insertion preserves the approximant condition of all stored rows.

theorem CompPoly.PolynomialMatrix.Approximant.pivotRows_approximates {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (mulCtx : CPolynomial.MulContext F) (problem : XAdicProblem F) {pivots : Array (Option (PolynomialRow F))} (hpivots : ∀ (p : ℕ) (r : PolynomialRow F), pivots.getD p none = some r → RowApproximates mulCtx problem r) {row : PolynomialRow F} (hrow : row ∈ (pivotRows pivots).MatrixRows) : RowApproximates mulCtx problem row

Rows extracted from a sound pivot table satisfy the approximant condition.

theorem CompPoly.PolynomialMatrix.Approximant.reduceKernelLeafRowsByPivots_approximates {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (mulCtx : CPolynomial.MulContext F) (problem : XAdicProblem F) {rows : PolynomialMatrix F} (shift : Array ℕ) (hrows : ∀ row ∈ rows.MatrixRows, RowApproximates mulCtx problem row) {row : PolynomialRow F} (hrow : row ∈ (reduceKernelLeafRowsByPivots rows shift).MatrixRows) : RowApproximates mulCtx problem row

Pivot-table reduction preserves the approximant condition.

theorem CompPoly.PolynomialMatrix.Approximant.compactNonzeroRows_subset {F : Type u_1} [Field F] [BEq F] {rows : PolynomialMatrix F} {row : PolynomialRow F} (hrow : row ∈ (compactNonzeroRows rows).MatrixRows) : row ∈ rows.MatrixRows

Compaction preserves row membership soundness.

theorem CompPoly.PolynomialMatrix.Approximant.compactNonzeroRows_nonzero {F : Type u_1} [Field F] [BEq F] {rows : PolynomialMatrix F} {row : PolynomialRow F} (hrow : row ∈ (compactNonzeroRows rows).MatrixRows) : rowIsZero row = false

Compacted rows are nonzero.

theorem CompPoly.PolynomialMatrix.Approximant.coeffXPower_toPoly {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (c : F) (d : ℕ) : (coeffXPower c d).toPoly = Polynomial.C c * Polynomial.X ^ d

The monomial coeffXPower c d under toPoly.

theorem CompPoly.PolynomialMatrix.Approximant.rowApproximates_monomialUnitRow {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (mulCtx : CPolynomial.MulContext F) (problem : XAdicProblem F) {i d : ℕ} (hd : ∀ j < problem.orders.size, problem.orders.getD j 0 ≤ d) : RowApproximates mulCtx problem (monomialUnitRow (Array.size problem.matrix) i d)

Monomial unit rows of sufficiently high degree satisfy every X-adic condition.

theorem CompPoly.PolynomialMatrix.Approximant.getD_le_maxOrder {F : Type u_1} [Field F] (problem : XAdicProblem F) {j : ℕ} (hj : j < problem.orders.size) : problem.orders.getD j 0 ≤ maxOrder problem

Every entry of the order vector is bounded by maxOrder.

theorem CompPoly.PolynomialMatrix.Approximant.missingCompletionRows_approximates {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (mulCtx : CPolynomial.MulContext F) (problem : XAdicProblem F) (shift : Array ℕ) (rows : PolynomialMatrix F) {row : PolynomialRow F} (hrow : row ∈ (missingCompletionRows problem shift rows).MatrixRows) : RowApproximates mulCtx problem row

Missing-pivot completion rows satisfy every X-adic condition.

theorem CompPoly.PolynomialMatrix.Approximant.completeMissingPivotRows_approximates {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (mulCtx : CPolynomial.MulContext F) (problem : XAdicProblem F) (shift : Array ℕ) {rows : PolynomialMatrix F} (hrows : ∀ row ∈ rows.MatrixRows, RowApproximates mulCtx problem row) {row : PolynomialRow F} (hrow : row ∈ (completeMissingPivotRows problem shift rows).MatrixRows) : RowApproximates mulCtx problem row

Pivot completion preserves the approximant condition.

Composition soundness

theorem CompPoly.PolynomialMatrix.Approximant.divXTrunc_coeff {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (shift order : ℕ) (p : CPolynomial F) (t : ℕ) : (divXTrunc shift order p).coeff t = if t < order then p.coeff (t + shift) else 0

Coefficients of the shifted truncation divXTrunc.

theorem CompPoly.PolynomialMatrix.Approximant.rowMulMatrixWith_ctx {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (ctx₁ ctx₂ : CPolynomial.MulContext F) (row : PolynomialRow F) (M : PolynomialMatrix F) : rowMulMatrixWith ctx₁ row M = rowMulMatrixWith ctx₂ row M

The row-by-matrix product does not depend on the multiplication context.

theorem CompPoly.PolynomialMatrix.Approximant.natArray_map_getD (f : ℕ → ℕ) (a : Array ℕ) {j : ℕ} (hj : j < a.size) : (Array.map f a).getD j 0 = f (a.getD j 0)

getD of a mapped natural-number array at an in-bounds index.

theorem CompPoly.PolynomialMatrix.Approximant.matrixWidth_eq_of_first_row {F : Type u_1} [Field F] {M : PolynomialMatrix F} {n : ℕ} (hne : 0 < Array.size M) (hsize : ∀ r ∈ M.MatrixRows, Array.size r = n) : M.MatrixWidth = n

A nonempty matrix with uniform row width n has MatrixWidth n.

theorem CompPoly.PolynomialMatrix.Approximant.getD_mem_matrixRows {F : Type u_1} [Field F] {M : PolynomialMatrix F} {l : ℕ} (hl : l < Array.size M) : Array.getD M l #[] ∈ M.MatrixRows

In-bounds getD rows are matrix rows.

theorem CompPoly.PolynomialMatrix.Approximant.rowApproximates_composed {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (mulCtx : CPolynomial.MulContext F) {problem : XAdicProblem F} {d₁ : ℕ} {P₁ Rmat : PolynomialMatrix F} (hP₁ : ∀ r ∈ P₁.MatrixRows, RowApproximates mulCtx { orders := lowerOrders problem d₁, matrix := problem.matrix } r ∧ Array.size r = Array.size problem.matrix) (hRsize : Array.size Rmat = Array.size P₁) (hRwidth : 0 < Array.size P₁ → problem.matrix.MatrixWidth ≤ Rmat.MatrixWidth) (hR : ∀ (l j : ℕ), l < Array.size P₁ → j < problem.orders.size → j < problem.matrix.MatrixWidth → ∀ t < problem.orders.getD j 0 - d₁, (rowGet (Array.getD Rmat l #[]) j).coeff t = (rowGet (rowMulMatrixWith mulCtx (Array.getD P₁ l #[]) problem.matrix) j).coeff (t + d₁)) {p₂ : PolynomialRow F} (hp₂ : RowApproximates mulCtx { orders := residualOrders problem d₁, matrix := Rmat } p₂) : RowApproximates mulCtx problem (rowMulMatrixWith mulCtx p₂ P₁)

Soundness of one PM-basis composition step: a residual-approximant row times a lower-approximant basis approximates the full problem.