Approximant-Basis Correctness Surface #
Named theorem surface for X-adic approximant bases and diagonal modular solution bases. The executable contexts carry the current proof obligations.
theorem
CompPoly.PolynomialMatrix.Approximant.modularSolutionBasis_sound
{F : Type u_1}
[Field F]
[BEq F]
[LawfulBEq F]
(ctx : ModularSolutionBasisContext F)
(equation : ModularEquation F)
(shift : Array ℕ)
(degreeBound? : Option ℕ)
{row : PolynomialRow F}
(hrow : row ∈ (ctx.solutionBasis equation shift degreeBound?).MatrixRows)
:
Rows returned by a modular solution-basis context satisfy the modular equation.
theorem
CompPoly.PolynomialMatrix.Approximant.modularSolutionBasis_complete_minimal
{F : Type u_1}
[Field F]
[BEq F]
[LawfulBEq F]
(ctx : ModularSolutionBasisContext F)
(equation : ModularEquation F)
(shift : Array ℕ)
(degreeBound? : Option ℕ)
{row : PolynomialRow F}
{rowDegree : ℕ}
(hmonic : ∀ b < equation.moduli.size, (equation.moduli.getD b 0).monic = true)
(hcols : equation.moduli.size ≤ equation.matrix.MatrixWidth)
(hshift : shift.size = equation.solutionWidth)
(hrow : rowSatisfiesModularBool ctx.mulContext ctx.modContext row equation.matrix equation.moduli = true)
(hnonzero : rowIsZero row = false)
(hwidth : Array.size row ≤ equation.solutionWidth)
(hdegree : rowShiftedDegree? row shift = some rowDegree)
(hbound : ∀ (bound : ℕ), degreeBound? = some bound → rowDegree ≤ bound)
:
(∀ basisRow ∈ (ctx.solutionBasis equation shift degreeBound?).MatrixRows,
Array.size basisRow ≤ equation.solutionWidth) ∧ ∃ (basisRow : PolynomialRow F) (degree : ℕ),
basisRow ∈ (ctx.solutionBasis equation shift degreeBound?).MatrixRows ∧ rowShiftedDegree? basisRow shift = some degree ∧ degree ≤ degreeBound?.getD rowDegree
Solution-basis completeness/minimality contract, relative to the
caller-supplied degree bound: a solution row within the bound (vacuous for
none) is matched by a returned basis row whose shifted degree does not
exceed the bound — the solution's own degree when no bound is supplied.