Filtered Modular Solver Completeness

Completeness/minimality of the filtered PM-basis modular solver: every nonzero in-width solution of a monic diagonal modular equation is dominated by a returned row, via the certified verification window.

Completeness/minimality of the filtered PM-basis modular solver

The argument routes every modular solution through the certified verification window. A nonzero in-width solution row of shifted degree e ≤ bound lifts to an exact row of the reduced exact-nullspace problem whose expanded shifted degree is at most e + bound + 1. The PM-basis minimality contract yields a basis row of dominated expanded degree, the verification orders force its column products to vanish exactly, and its principal truncation is therefore a modular solution of shifted degree at most e surviving both filters. Solutions above the verification window are handled either by the adaptive rows themselves or by falling back to the always-available solution e_p * prod(moduli), which fits the saturated window.

Generic access and summation helpers

theorem CompPoly.PolynomialMatrix.Approximant.me_getD_mem_toList {α : Type u_2} {xs : Array α} {i : ℕ} (d : α) (hi : i < xs.size) : xs.getD i d ∈ xs.toList

In-bounds getD values are list members.

Zero-row and shifted-degree helpers

theorem CompPoly.PolynomialMatrix.Approximant.me_rowShiftedDegree_isSome {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] {row : PolynomialRow F} {shift : Array ℕ} (hnz : rowIsZero row = false) : ∃ (d : ℕ), rowShiftedDegree? row shift = some d

Nonzero rows have a shifted degree.

maxShiftDegree and modulus-product bounds

Modular-reduction semantics (local copies of the GS bridge lemmas)

Membership plumbing for the pipeline filters

theorem CompPoly.PolynomialMatrix.Approximant.me_filterModularSolutionRows_subset {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] {mulCtx : CPolynomial.MulContext F} {modCtx : CPolynomial.ModContext F} {equation : ModularEquation F} {rows : PolynomialMatrix F} {row : PolynomialRow F} (hrow : row ∈ (filterModularSolutionRows mulCtx modCtx equation rows).MatrixRows) : row ∈ rows.MatrixRows

Filtered modular-solution rows come from the input rows.

theorem CompPoly.PolynomialMatrix.Approximant.me_principalSolutionRows_width {F : Type u_1} [Field F] {sW : ℕ} {basis : PolynomialMatrix F} {row : PolynomialRow F} (hrow : row ∈ (principalSolutionRows sW basis).MatrixRows) : Array.size row = sW

Principal solution rows keep the basis row width.

Width discipline of the adaptive pipeline

theorem CompPoly.PolynomialMatrix.Approximant.me_adaptiveBasis_width {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] {mulCtx : CPolynomial.MulContext F} {modCtx : CPolynomial.ModContext F} {pmCtx : PMBasisContext F} {equation : ModularEquation F} {shift : Array ℕ} {degreeBound? : Option ℕ} (r : PolynomialRow F) : r ∈ (adaptiveSolutionBasis mulCtx modCtx pmCtx equation shift degreeBound?).filtered.MatrixRows → Array.size r = equation.solutionWidth

Every adaptive solution-basis row has the linearized width.

The fallback solution e_p * prod(moduli)

theorem CompPoly.PolynomialMatrix.Approximant.me_prodRow_facts {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (mulCtx : CPolynomial.MulContext F) (modCtx : CPolynomial.ModContext F) (equation : ModularEquation F) (shift : Array ℕ) {p : ℕ} (hmonic : ∀ b < equation.moduli.size, (equation.moduli.getD b 0).monic = true) (hcols : equation.moduli.size ≤ equation.matrix.MatrixWidth) (hp : p < equation.solutionWidth) : ∃ (prow : PolynomialRow F) (e : ℕ), rowSatisfiesModularBool mulCtx modCtx prow equation.matrix equation.moduli = true ∧ rowIsZero prow = false ∧ Array.size prow = equation.solutionWidth ∧ rowShiftedDegree? prow shift = some e ∧ e ≤ pivotWindowCap equation + maxShiftDegree shift

Structure of the fallback row e_p * prod(moduli).

The certified verification window

theorem CompPoly.PolynomialMatrix.Approximant.me_verification_dominates {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (mulCtx : CPolynomial.MulContext F) (modCtx : CPolynomial.ModContext F) (pmCtx : PMBasisContext F) (equation : ModularEquation F) (shift : Array ℕ) (bound : ℕ) {rowStar : PolynomialRow F} {e : ℕ} (hmonic : ∀ b < equation.moduli.size, (equation.moduli.getD b 0).monic = true) (hcols : equation.moduli.size ≤ equation.matrix.MatrixWidth) (hshift : shift.size = equation.solutionWidth) (hpos : 0 < equation.solutionWidth) (hsat : rowSatisfiesModularBool mulCtx modCtx rowStar equation.matrix equation.moduli = true) (hnz : rowIsZero rowStar = false) (hwidth : Array.size rowStar ≤ equation.solutionWidth) (hdeg : rowShiftedDegree? rowStar shift = some e) (hebound : e ≤ bound) : ∃ (basisRow : PolynomialRow F) (degree : ℕ), basisRow ∈ (filterModularSolutionRows mulCtx modCtx equation (compactNonzeroRows (principalSolutionRows equation.solutionWidth (pmCtx.basis (fullWindowExactNullspaceProblem modCtx equation bound) (exactNullspaceShift shift equation.modularWidth bound))))).MatrixRows ∧ rowShiftedDegree? basisRow shift = some degree ∧ degree ≤ e

Certified-window domination: any nonzero in-width modular solution row whose shifted degree fits inside the verification window bound is degree-dominated by a row of the filtered verification basis.