feat(linalg): order-basis approximant layer over polynomial matrices by dhsorens · Pull Request #312 · Verified-zkEVM/CompPoly

dhsorens · 2026-09-02T14:13:40Z

The linear-algebra half of olympichek's (Valerii Huhnin) Guruswami-Sudan approximant
work from #255, split out of #291 so it can be reviewed on its own. Their commit
authorship is preserved; the port to current main is a separate commit.

Why split

#291 is 14,022 lines, of which roughly 10,800 are this layer and only ~2,600 the
Guruswami-Sudan interpolation backends that consume it. This half sits under ROADMAP
item 10 (computable linear algebra) and has no dependency on Bivariate/ at all —
verified: none of these 23 files references Bivariate, GuruswamiSudan or GSInterp.
Reviewing it separately is what makes either half tractable.

The GS interpolation backends follow in a second PR, stacked on this one.

Stack

main
 └── #290 re-land/roots-shoup-lasvegas   (Shoup + Las Vegas roots)
      └── this PR restack/pm-approximant  (order-basis layer)
           └── GS approximant + hybrid interpolation (to follow)

Merge #290 first. GitHub retargets this to main automatically once it lands.

ModularEquation/ — modular key equations, soundness and completeness
PMBasis/ — the divide-and-conquer order-basis recursion, with X-adic soundness,
kernel-leaf soundness/completeness, and the scalar and span kernel-leaf layers
PartialLinearization.lean — degree balancing for the recursion

plus the supporting matrix pieces the recursion needs: Operations.lean,
RowSelection.lean, StrassenCorrectness.lean (fast multiplication, genuinely
load-bearing — PMBasis/Recursion, ModularEquation/Basic and XAdicSoundness all
consume it), and MuldersStorjohannCorrectness/WeakPopovMinimal.lean.

Port to current main

The original was written against Lean 4.32.0; main is on 4.33.1. No proof content
needed repair — the failures were all module-system exposure:

import all for the same-package implementation dependencies these proofs step
through (Univariate.Basic, Univariate.Raw.Core). coeff, ofArray and the Raw
wrappers sit in bare public sections, so their bodies are opaque downstream and
rw [CPolynomial.ofArray], simp [Raw.coeff] and p.coeff i = (↑p).coeff i := rfl
stopped working. This is the pattern docs/wiki/module-system.md prescribes.
letI to let per the haveILetI style linter.

All 23 files carry module, public import and @[expose] public section; the test
module uses public meta.

Verification

lake build (no new warnings), lake test, ./scripts/lint-style.sh,
./scripts/check-imports.sh, python3 ./scripts/check-docs-integrity.py and
lake exe axiomsweep --check all pass.

The sweep reports 0 sorryAx-tainted and 0 non-standard-axiom-tainted declarations
across 324 modules, and the committed baseline needs no refresh. No native_decide, no
@[extern].

Note

No benchmark here — this layer has no standalone entry point to time. The asymptotic
claim it exists to support ("quasi-linear, independent of corruption level") is a
property of the GS backend, so the guruswami-sudan-approximant-* bench group lands
with that PR.

github-actions · 2026-09-02T14:19:32Z

Build Timing Report

Commit: 684604a
Message: Merge 3fec4ad into 19f0794
Ref: restack/pm-approximant
Comparison baseline: c589a82 from the previous successful PR update.
Measured on ubuntu-latest with /usr/bin/time -p.
Commands: library build (warm) lake build; test path lake test.
Clean build was skipped (warm/incremental CI; no toolchain or lake-manifest change). Runs automatically when lean-toolchain or lake-manifest.json changes, or via Actions → Lean Action CI → Run workflow with clean_build.

Measurement	Baseline (s)	Current (s)	Delta (s)	Status
Library build (warm)	44.90	1.70	-43.20	ok
Test path	7.69	1.39	-6.30	ok

Incremental Rebuild Signal

Warm-only run: default CI reuses cached oleans and rebuilds dirty modules only. No same-job clean:warm ratio.

Slowest Current Build Files (warm library build)

No per-target timings were parsed from the current warm library build log.

github-actions · 2026-09-02T14:19:38Z

🤖 PR Summary

This PR introduces the order-basis (approximant) layer over polynomial matrices, split from a larger Guruswami–Sudan interpolation PR (#291). It provides a fully formalized, executable, and correctness-proven implementation of a divide-and-conquer PM-basis algorithm, along with supporting matrix operations and modular equation solving. The layer is a prerequisite for the Guruswami–Sudan decoder and sits under ROADMAP item 10 (computable linear algebra). All theorems are fully proved; no sorry or admit appear anywhere in the codebase.

Statistics

Metric	Count
📝 Files Changed	27
✅ Lines Added	11384
❌ Lines Removed	5

Lean Declarations

✏️ Added: 575 declaration(s)

CompPoly/LinearAlgebra/PolynomialMatrix/Approximant/Basic.lean (7)

def lowerOrders [Zero F] (problem : XAdicProblem F) (d : Nat) : Array Nat
def maxOrder [Zero F] (problem : XAdicProblem F) : Nat
def residualMatrix [Semiring F] [BEq F] [LawfulBEq F]
def residualMatrixWithProduct [Semiring F] [BEq F] [LawfulBEq F]
def residualOrders [Zero F] (problem : XAdicProblem F) (d : Nat) : Array Nat
def totalOrder [Zero F] (problem : XAdicProblem F) : Nat
def updateShiftByRows [Zero F] [BEq F]

CompPoly/LinearAlgebra/PolynomialMatrix/Approximant/Correctness.lean (2)

theorem modularSolutionBasis_complete_minimal
theorem modularSolutionBasis_sound

CompPoly/LinearAlgebra/PolynomialMatrix/Approximant/ModularEquation.lean (1)

def modularSolutionBasisContextViaPMBasis

CompPoly/LinearAlgebra/PolynomialMatrix/Approximant/ModularEquation/Basic.lean (53)

def ModularEquation.modularWidth (equation : ModularEquation F) : Nat
def ModularEquation.solutionWidth (equation : ModularEquation F) : Nat
def PivotDegreeProfile.coversAll (profile : PivotDegreeProfile) : Bool
def PivotDegreeProfile.discoveredAny (profile : PivotDegreeProfile) : Bool
def PivotDegreeProfile.insert (profile : PivotDegreeProfile)
def adaptiveProfileDegrees (shift : Array Nat) (profile : PivotDegreeProfile)
def adaptiveSolutionBasis
def adaptiveSolutionLoop
def adaptiveSolutionRound
def allCoordinatesSettled (profile : PivotDegreeProfile) (budgets : Array Nat)
def candidateRowShift (rows : PolynomialMatrix F) (shift : Array Nat) : Array Nat
def chunkedExactNullspaceLift (modCtx : CPolynomial.ModContext F)
def chunkedExactNullspaceProblem (modCtx : CPolynomial.ModContext F)
def chunkedExactNullspaceProblemForShift (modCtx : CPolynomial.ModContext F)
def chunkedLiftOrders (delta modularWidth : Nat)
def chunkedPrincipalRows (modCtx : CPolynomial.ModContext F)
def coordinateSettled (profile : PivotDegreeProfile) (budgets : Array Nat)
def debugUnchunkedFilteredSolutionBasisViaPMBasis
def degreeGatePassed (degreeBound? bestDegree? : Option Nat) : Bool
def discoverPivotDegreeProfileViaPMBasis
def emptyPivotDegreeProfile (solutionWidth : Nat) : PivotDegreeProfile
def escalateUnsettledBudgets (profile : PivotDegreeProfile)
def exactNullspaceLift (equation : ModularEquation F) : PolynomialMatrix F
def exactNullspaceProblem (equation : ModularEquation F) : XAdicProblem F
def filterModularSolutionRows
def filteredSolutionBasisViaPMBasis
def fullWindowDegreeBound (equation : ModularEquation F)
def fullWindowExactNullspaceProblem (modCtx : CPolynomial.ModContext F)
def fullWindowSolutionBasisViaPMBasis (modCtx : CPolynomial.ModContext F)
def gatedWindowBound (equation : ModularEquation F)
def knownDegreeFilteredSolutionBasisViaPMBasis
def knownDegreeSolutionBasisViaPMBasis (modCtx : CPolynomial.ModContext F)
def leastSolutionRowDegree? (rows : PolynomialMatrix F) (shift : Array Nat) :
def modularResidualRows
def negativeDiagonalRows (moduli : Array (CPolynomial F)) : PolynomialMatrix F
def pivotDegreeProfileFromRows (solutionWidth : Nat)
def pivotDegreeProfileMergeRows (profile : PivotDegreeProfile)
def pivotWindowCap (equation : ModularEquation F) : Nat
def principalSolutionRows (solutionWidth : Nat) (basis : PolynomialMatrix F) :
def reducedExactNullspaceLift (modCtx : CPolynomial.ModContext F)
def repairSolutionRowsViaPMBasis
def solutionBasisViaPMBasis (modCtx : CPolynomial.ModContext F)
def solutionBasisWithPlanViaPMBasis (modCtx : CPolynomial.ModContext F)
def unchunkedSolutionBasisViaPMBasis (modCtx : CPolynomial.ModContext F)
def verificationSolutionBasisViaPMBasis (modCtx : CPolynomial.ModContext F)
def verificationWindowBound (equation : ModularEquation F)
def windowedSolutionBasisViaPMBasis (modCtx : CPolynomial.ModContext F)
theorem adaptiveSolutionBasis_filtered_sound
theorem adaptiveSolutionLoop_filtered_sound
theorem adaptiveSolutionRound_filtered_sound
theorem degreeGatePassed_eq_true_iff {degreeBound? bestDegree? : Option Nat} :
theorem filteredSolutionBasisViaPMBasis_sound
theorem rowSatisfiesModularBool_of_mem_filterModularSolutionRows

CompPoly/LinearAlgebra/PolynomialMatrix/Approximant/ModularEquation/Completeness.lean (47)

private def me_moduliProduct (moduli : Array (CPolynomial F)) : CPolynomial F
private theorem me_adaptiveLoop_width
private theorem me_adaptiveRound_width
private theorem me_divByMonic_mul_eq {p M : CPolynomial F} (hM : M.monic)
private theorem me_dvd_modByMonicWith_sub (modCtx : CPolynomial.ModContext F)
private theorem me_entry_le_of_rowShiftedDegree {row : PolynomialRow F}
private theorem me_eq_zero_of_X_pow_dvd_of_natDegree_lt {p : Polynomial F} {n : Nat}
private theorem me_foldl_add_mono :
private theorem me_foldl_max_init_le (g : Nat → Nat) :
private theorem me_foldl_mul_natDegree_le :
private theorem me_foldl_mul_toPoly :
private theorem me_getD_append_left {α : Type*} {A B : Array α} {i : Nat} (d : α)
private theorem me_getD_append_right {α : Type*} {A B : Array α} {i : Nat} (d : α)
private theorem me_getD_list_range_map {α : Type*} (g : Nat → α) (n j : Nat) (d : α) :
private theorem me_getD_replicate {α : Type*} {n : Nat} (a d : α) {i : Nat}
private theorem me_le_foldl_max (g : Nat → Nat) :
private theorem me_list_prod_ne_zero :
private theorem me_matrixWidth_eq_getD (M : PolynomialMatrix F) :
private theorem me_mem_compactNonzeroRows {rows : PolynomialMatrix F}
private theorem me_mem_filterModularSolutionRows
private theorem me_mem_principalSolutionRows {sW : Nat} {basis : PolynomialMatrix F}
private theorem me_modByMonicWith_eq_zero_iff_dvd (modCtx : CPolynomial.ModContext F)
private theorem me_modByMonicWith_toPoly (modCtx : CPolynomial.ModContext F)
private theorem me_moduliProduct_dvd {moduli : Array (CPolynomial F)} {b : Nat}
private theorem me_moduliProduct_natDegree_le (moduli : Array (CPolynomial F)) :
private theorem me_moduliProduct_ne_zero {moduli : Array (CPolynomial F)}
private theorem me_moduliProduct_toPoly (moduli : Array (CPolynomial F)) :
private theorem me_natDegree_sum_le {n : Nat} (f : Nat → Polynomial F) {D : Nat}
private theorem me_rowGet_eq_zero_of_rowIsZero {row : PolynomialRow F}
private theorem me_rowIsZero_false_of_entry {row : PolynomialRow F} {j : Nat}
private theorem me_rowIsZero_of_forall {row : PolynomialRow F}
private theorem me_rowMul_toPoly (mulCtx : CPolynomial.MulContext F)
private theorem me_rowSatisfies_iff (mulCtx : CPolynomial.MulContext F)
private theorem me_rowShiftedDegree_attained {row : PolynomialRow F}
private theorem me_shift_le_maxShiftDegree (shift : Array Nat) (j : Nat) :
private theorem me_shiftedEntryDegree_eq {row : PolynomialRow F} {shift : Array Nat}
private theorem me_shiftedEntryDegree_some {row : PolynomialRow F} {shift : Array Nat}
private theorem me_solutionBasisWithPlan_width
private theorem me_sum_range_add {M : Type*} [AddCommMonoid M] (f : Nat → M)
private theorem me_toPoly_sum (f : Nat → CPolynomial F) (n : Nat) :
theorem me_adaptiveBasis_width
theorem me_filterModularSolutionRows_subset
theorem me_getD_mem_toList {α : Type*} {xs : Array α} {i : Nat} (d : α)
theorem me_principalSolutionRows_width {sW : Nat}
theorem me_prodRow_facts (mulCtx : CPolynomial.MulContext F)
theorem me_rowShiftedDegree_isSome {row : PolynomialRow F} {shift : Array Nat}
theorem me_verification_dominates

CompPoly/LinearAlgebra/PolynomialMatrix/Approximant/PMBasis.lean (3)

def kernelLeafPMBasisContext (mulCtx : CPolynomial.MulContext F)
def kernelLeafPMBasisContextWithLow (mulCtx : CPolynomial.MulContext F)
def kernelLeafPMBasisContextWithLowAndCompose (mulCtx : CPolynomial.MulContext F)

CompPoly/LinearAlgebra/PolynomialMatrix/Approximant/PMBasis/Correctness.lean (30)

private theorem pm_coeffXPower_one_natDegree (d : Nat) :
private theorem pm_coeffXPower_one_ne_zero (d : Nat) :
private theorem pm_combination_mul_toPoly (mulCtx : CPolynomial.MulContext F)
private theorem pm_completeMissingPivotRows_shiftedWeakPopov [DecidableEq F]
private theorem pm_eq_of_toPoly_eq {a b : CPolynomial F}
private theorem pm_mem_matrixRows_compactNonzeroRows {X : PolynomialMatrix F}
private theorem pm_mem_rowSpan_compactNonzeroRows [DecidableEq F]
private theorem pm_mem_rowSpan_of_nonzero_rows_mem [DecidableEq F]
private theorem pm_missingCompletionRows_facts [DecidableEq F]
private theorem pm_missingCompletionRows_pairwise [DecidableEq F]
private theorem pm_pivotRows_shiftedWeakPopov
private theorem pm_rowApproximates_append_replicate
private theorem pm_rowApproximates_residual_of_combination
private theorem pm_rowGet_append_replicate (row : PolynomialRow F)
private theorem pm_rowGet_eq_zero_of_rowIsZero {row : PolynomialRow F}
private theorem pm_rowIsZero_of_mem_rowSpan_all_zero {X : PolynomialMatrix F}
private theorem pm_rowIsZero_of_rowGet {row : PolynomialRow F}
private theorem pm_rowLinearCombination_combination
private theorem pm_rowShiftedDegree_append_replicate (row : PolynomialRow F)
private theorem pm_rowShiftedDegree_monomialUnitRow {n i : Nat} (cap : Nat)
private theorem pm_rowShiftedLeadingPosition_monomialUnitRow [DecidableEq F]
private theorem pm_rowsContainLeadingPosition_of_getD
private theorem pm_shiftedEntryDegree_congr {row row' : PolynomialRow F}
private theorem pm_shiftedEntryDegree_eq_none_of_rowGet_eq_zero
private theorem pm_shiftedEntryDegree_monomialUnitRow_ne {n i j : Nat}
private theorem pm_shiftedEntryDegree_monomialUnitRow_self {n i : Nat}
theorem pmBasisWithFuelCore_kernelLeaf_rowSpan_complete [DecidableEq F]
theorem pmBasisWithFuelCore_kernelLeaf_rows (mulCtx : CPolynomial.MulContext F)
theorem pmBasis_kernelLeaf_approximates (mulCtx : CPolynomial.MulContext F)
theorem pmBasis_kernelLeaf_complete_minimal [DecidableEq F]

CompPoly/LinearAlgebra/PolynomialMatrix/Approximant/PMBasis/KernelLeaf.lean (39)

def addScaledScalarRow (target source : Array F) (factor : F) : Array F
def basisVectorForFreeColumnRows (rows : Array (Array F))
def cancelKernelLeafLeadingTerm
def coeffXPower (c : F) (d : Nat) : CPolynomial F
def coefficientEquationIndices (orders : Array Nat) : Array (Nat × Nat)
def coefficientMatrix (problem : XAdicProblem F) : DenseMatrix F
def coefficientMatrixRow (problem : XAdicProblem F) (degreeCap : Nat)

…and 425 more not listed.

sorry Tracking

No sorrys were added, removed, or affected.

Coverage Notes

Additional-instructions analysis was skipped because the full diff exceeded the analysis size budget, and partial results would be misleading.

📄 **Per-File Summaries**

CompPoly.lean: This change adds a large block of public import statements to CompPoly.lean, exposing the newly created CompPoly.LinearAlgebra.PolynomialMatrix.Approximant module hierarchy (including Basic, Correctness, ModularEquation with Completeness, PMBasis with multiple submodules such as KernelLeaf, KernelLeafSoundness, KernelLeafCompleteness, KernelLeafScalar, KernelLeafSpan, Recursion, XAdicSoundness, and PartialLinearization), as well as several other new modules: CompPoly.LinearAlgebra.PolynomialMatrix.MuldersStorjohannCorrectness.WeakPopovMinimal, CompPoly.LinearAlgebra.PolynomialMatrix.Operations, CompPoly.LinearAlgebra.PolynomialMatrix.RowSelection, and CompPoly.LinearAlgebra.PolynomialMatrix.StrassenCorrectness. No existing imports were removed or modified, and the diff contains no sorry or admit; it solely extends the set of modules publicly re‑exported by this file.
CompPoly/LinearAlgebra/PolynomialMatrix.lean: The file now publicly imports and re-exports CompPoly.LinearAlgebra.PolynomialMatrix.Operations and CompPoly.LinearAlgebra.PolynomialMatrix.Approximant, adding their definitions and theorems to the public API of PolynomialMatrix alongside the existing re-exports of Basic, Degree, Shifted, RowSpan, and ShiftedReduction.
CompPoly/LinearAlgebra/PolynomialMatrix/Approximant.lean: Added a new top-level module Approximant.lean that re-exports five submodules — Basic, PMBasis, PartialLinearization, ModularEquation, and Correctness — via public import. The file also declares an @[expose] public section (though no new definitions or theorems are provided). This consolidates the Approximant infrastructure into a single import target, simplifying downstream usage of the polynomial-matrix approximant theory.
CompPoly/LinearAlgebra/PolynomialMatrix/Approximant/Basic.lean: This new file introduces the XAdicProblem structure for representing row approximant problems, containing fields orders and matrix. Several utility functions are defined: maxOrder and totalOrder compute the maximum and total X-adic orders; lowerOrders truncates each order to at most d, while residualOrders subtracts d from each order; updateShiftByRows adjusts a shift array based on row-shifted degrees from a basis matrix; residualMatrixWithProduct computes the residual matrix (P * A) div X^d truncated to given residual orders using a product kernel, and residualMatrix is a specific variant using the direct low-product row-column kernel via PolynomialMatrix.mulTruncColumnWith. No sorry or admit are present.
CompPoly/LinearAlgebra/PolynomialMatrix/Approximant/Correctness.lean: This new file Correctness.lean adds two theorems, modularSolutionBasis_sound and modularSolutionBasis_complete_minimal, that form a named theorem surface for X-adic approximant bases and diagonal modular solution bases. The first theorem states that every row in the solution basis returned by a ModularSolutionBasisContext satisfies the corresponding modular equation. The second theorem establishes a completeness/minimality contract: for any non‑zero solution row respecting the degree bound (or unbounded), there exists a basis row whose shifted degree does not exceed the bound. Both theorems are proven by delegating to the corresponding methods of the context (ctx.sound and ctx.complete_minimal).
CompPoly/LinearAlgebra/PolynomialMatrix/Approximant/ModularEquation.lean: This new file (ModularEquation.lean) adds the modularSolutionBasisContextViaPMBasis definition, which constructs a ModularSolutionBasisContext from a MulContext, ModContext, and PMBasisContext. The definition provides both the sound property (delegating to filteredSolutionBasisViaPMBasis_sound) and the complete_minimal property, whose proof performs an exhaustive case analysis on degreeGatePassed to show that for any admissible solution row there exists a basis row matching the degree bound. The file also publicly imports Completeness.lean and acts as an umbrella module for the diagonal modular‑equation solver development. No sorry or admit appear in the diff.
CompPoly/LinearAlgebra/PolynomialMatrix/Approximant/ModularEquation/Basic.lean: This new file introduces the ModularEquation data structure (moduli and matrix) and the full solver pipeline for diagonal modular equations in the polynomial matrix approximant framework. It defines chunked exact‑nullspace problems (chunkedExactNullspaceProblem, chunkedExactNullspaceProblemForShift), a PivotDegreeProfile for adaptive per‑coordinate window escalation, and a suite of solver entry points (adaptiveSolutionBasis, filteredSolutionBasisViaPMBasis, fullWindowSolutionBasisViaPMBasis, knownDegreeFilteredSolutionBasisViaPMBasis) that combine adaptive degree‑first search with a certified verification solve and a residual repair pass. Several soundness theorems are proved (e.g., filteredSolutionBasisViaPMBasis_sound), and the ModularSolutionBasisContext structure bundles the solver with its contract. No sorry or admit statements are present.
CompPoly/LinearAlgebra/PolynomialMatrix/Approximant/ModularEquation/Completeness.lean: This new file (1145 lines) proves the completeness of the filtered PM-basis modular solver for monic diagonal modular equations. The main theorem, me_verification_dominates, establishes that any nonzero solution row of width at most the solution width and shifted degree ≤ bound is degree-dominated by a row of the filtered verification basis. Supporting definitions include me_moduliProduct (the product of moduli) and me_prodRow_facts (structure of the fallback row e_p * prod(moduli)). Additional public theorems cover membership in filter/compact/principal rows, row sizes in adaptive rounds, and the width of principal solution rows. No sorry or admit appears.
CompPoly/LinearAlgebra/PolynomialMatrix/Approximant/PMBasis.lean: This new file CompPoly/LinearAlgebra/PolynomialMatrix/Approximant/PMBasis.lean defines three PMBasisContext instances backed by a recursive divide-and-conquer PM-basis driver with scalar dense-kernel leaves, public-importing the correctness development from CompPoly.LinearAlgebra.PolynomialMatrix.Approximant.PMBasis.Correctness. The entry point kernelLeafPMBasisContextWithLowAndCompose provides a full PMBasisContext whose runtime and basis are given by kernelLeafRuntimeWithLowAndCompose and pmBasis applied to it, with sound proved via pmBasis_kernelLeaf_approximates and complete_minimal via pmBasis_kernelLeaf_complete_minimal (the latter establishing the predictable-degree property of minimal approximant bases). Two convenience constructors are provided: kernelLeafPMBasisContextWithLow, which passes the same cutoff for both leaf and composition, and kernelLeafPMBasisContext, which derives low‑product context from a MulContext via PolynomialMatrix.MulLowContext.fromMulContext.
CompPoly/LinearAlgebra/PolynomialMatrix/Approximant/PMBasis/Correctness.lean: This new file establishes the correctness of the kernel-leaf recursive PM-basis for X-adic approximants over polynomial matrices. The main theorems are:

pmBasisWithFuelCore_kernelLeaf_rows: every row of the fuel-bounded core approximates the problem and has the principal row width.
pmBasis_kernelLeaf_approximates: every row of the full (unbounded-fuel) recursive basis satisfies the X-adic approximant conditions.
pmBasisWithFuelCore_kernelLeaf_rowSpan_complete (generation completeness): every nonzero solution row lies in the row module spanned by the fuel-bounded core.
pmBasis_kernelLeaf_complete_minimal (shifted minimality): for any nonzero solution row padded to the principal width, some row of the root-normalized recursive basis has a shifted row degree that dominates it.

Supporting private lemmas include zero-row characterizations (pm_rowGet_eq_zero_of_rowIsZero, pm_rowIsZero_of_rowGet), span-transfers for zero-row compaction (pm_mem_rowSpan_compactNonzeroRows, pm_mem_rowSpan_of_nonzero_rows_mem), a combination-to-product rewrite (pm_rowLinearCombination_combination), a converse of the composition soundness step (pm_rowApproximates_residual_of_combination), and shape facts for monomial unit rows and missing-pivot completion (e.g., pm_rowShiftedLeadingPosition_monomialUnitRow, pm_completeMissingPivotRows_shiftedWeakPopov). No sorry or admit appears in the diff.

CompPoly/LinearAlgebra/PolynomialMatrix/Approximant/PMBasis/KernelLeaf.lean: This file introduces a new module defining the classical scalar-kernel PM-basis leaf for X-adic approximants. It provides executable algorithms to construct a dense scalar coefficient matrix from an XAdicProblem (via coefficientMatrix/coefficientMatrixRows), compute its row-array RREF kernel basis (via scalarRrefRows/homogeneousKernelBasisRows), convert kernel vectors back to polynomial rows (vectorToPolynomialRow), and complete the basis with monomial rows (kernelLeafCompletionRows, missingCompletionRows, completeMissingPivotRows). The file also contains two shifted-reduction engines—a conflict-scanning loop (reduceKernelLeafWithFuel) and a more efficient pivot-table inserter (insertKernelLeafPivotRowWithFuel/reduceKernelLeafRowsByPivots)—which are combined in an incremental insertion routine (reduceKernelLeafRowsIncremental). The top-level API kernelLeafBasis assembles these pieces to produce a reduced, completed polynomial-matrix basis for a given shift, and compactNonzeroRows removes zero rows before the basis enters a recursive residual computation. No sorry or admit appear in the diff.
CompPoly/LinearAlgebra/PolynomialMatrix/Approximant/PMBasis/KernelLeafCompleteness.lean: This new file, KernelLeafCompleteness.lean, proves the completeness of the kernel-leaf basis generation for X-adic problems. The main theorem, kernelLeafBasis_rowSpan_complete, states that every nonzero solution row lies in the row span of the kernel-leaf basis. It uses several private lemmas: pm_lowRow_mem_rowSpan_union (low part from scalar kernel completeness), pm_highRow_mem_rowSpan_union (high part from monomial completion rows), and pm_solution_mem_rowSpan_union (decomposition of a solution row into low and high parts). Supporting lemmas cover array operations (pm_append_getD_left, pm_append_getD_right, pm_map_getD), coefficient arithmetic (pm_coeff_C_mul, pm_coeff_finset_sum, pm_coeff_mul_coeffXPower), truncation (pm_truncateX_eq_zero_of_coeff, pm_high_factor), and row operations (pm_rowGet_monomialUnitRow, pm_completionRows_size, pm_completionRows_getD, pm_rowGet_rowLinearCombination, pm_rowLinearCombination_size, pm_row_ext, pm_rowApproximates_of_entry_dvd, pm_kernelLeafUnion_sizes, pm_reduceIncremental_sizes). No sorry or admit are present.
CompPoly/LinearAlgebra/PolynomialMatrix/Approximant/PMBasis/KernelLeafScalar.lean: This new file (1344 lines) introduces the scalar kernel leaf for the PM-basis, providing soundness and completeness of the homogeneous kernel computed via scalar RREF on row-array matrices. It defines scalarDot (coordinatewise dot product with zero defaults) and OrthRows (orthogonality to all rows), then proves elementary lemmas such as addScaledScalarRow_getD, normalizeScalarRow_getD, scalarDot_addScaledScalarRow, and scalarDot_eq_pivot_mul_normalize. The backward‑span theorem orthRows_of_scalarRrefRows shows that orthogonality to the RREF rows implies orthogonality to the original rows. A ScalarRrefSpec structure formalizes the RREF shape contract (strictly increasing pivot columns, unit columns, tail zeros) and is proven by scalarRrefRows_spec. The basis vector construction basisVectorForFreeColumnRows is analyzed with lemmas describing its entries. The main soundness theorem homogeneousKernelBasisRows_dot_eq_zero asserts that every vector in homogeneousKernelBasisRows is orthogonal to every input row, and the main completeness theorem homogeneousKernelBasisRows_complete states that any vector orthogonal to all input rows is an F‑linear combination (below cols) of the emitted basis vectors. No sorry or admit appear; the file is fully proved.
CompPoly/LinearAlgebra/PolynomialMatrix/Approximant/PMBasis/KernelLeafSoundness.lean: Added KernelLeafSoundness.lean, which proves the soundness of the kernel‑leaf basis: kernelLeafBasis_rows establishes that every row of kernelLeafBasis satisfies RowApproximates (the X‑adic approximant conditions) and has the principal row width. This relies on a new definition rowToCoefficientVector (packing polynomial coefficients into a flat scalar vector) and supporting lemmas that show bijectivity with vectorToPolynomialRow and that approximant rows yield orthogonality with the scalar coefficient rows. The proof uses invariant‑preservation theorems for the reduction and completion procedures (reduceKernelLeafRowsIncremental_invariant, pivotRows_invariant, etc.) and closes with coefficientMatrixRows_dot_eq_zero_of_approximates and the final kernelLeafBasis_rows theorem.
CompPoly/LinearAlgebra/PolynomialMatrix/Approximant/PMBasis/KernelLeafSpan.lean: This new file KernelLeafSpan.lean proves that the kernel‑leaf reduction (both the fuel‑based reduceKernelLeafRowsByPivots and the incremental reduceKernelLeafRowsIncremental) preserves the row span of the input polynomial matrix. It adds a battery of private supporting lemmas — showing that kernel‑leaf cancellation coincides with the Mulders–Storjohann cancellation (cancelKernelLeafLeadingTerm_eq_cancelShifted), that it decreases the shifted row measure (cancelKernelLeafLeadingTerm_shiftedRowMeasure_lt), and that pivot‑table insertion satisfies measure bounds and row‑span invariants (insertKernelLeafPivotRowWithFuel_rowSpan, insertKernelLeaf_foldl_rowSpan). The public theorems reduceKernelLeafRowsByPivots_rowSpan_superset and reduceKernelLeafRowsIncremental_rowSpan_superset assert that every nonzero row of the original matrix remains in the row span of the reduced matrix; reduceKernelLeafRowsByPivots_rows guarantees that each reduced row has the same width and is nonzero. Helper results rowIsZero_eq_zeroRow, size_pos_of_mem_matrixRows, wellFormed_of_sizes, and eq_empty_of_mem_rowSpan_empty establish basic properties of zero rows, matrix dimensions, and row spans. Several of these are stated with omit [BEq F] or omit [LawfulBEq F] to maximise generality. The file contains no sorry or admit.
CompPoly/LinearAlgebra/PolynomialMatrix/Approximant/PMBasis/Recursion.lean: This file introduces the recursive PM-basis driver for the CompPoly project. It defines the PMBasisRuntime structure, which bundles the multiplication context and leaf solver (kernelLeafBasis), along with factory functions kernelLeafRuntimeWithLowAndCompose, kernelLeafRuntimeWithLow, and kernelLeafRuntime. It implements the fuel-bounded divide-and-conquer recursion in pmBasisWithFuelCore, root normalization via pmBasisNormalizeRoot, and the entry-point functions pmBasisWithFuel, pmBasisFuel, and pmBasis. Two proof theorems, completeMissingPivotRows_size_pos and pmBasisNormalizeRoot_size_pos, guarantee that the output is nonempty for well-formed problems. Finally, the PMBasisContext structure packages the runtime with the basis function and the sound and complete_minimal specification theorems (stated but not proved in this file). No sorry or admit appears in the diff.
CompPoly/LinearAlgebra/PolynomialMatrix/Approximant/PMBasis/XAdicSoundness.lean: Adds the file XAdicSoundness.lean (~795 lines) which defines the RowApproximates predicate (RowApproximates mulCtx problem row) for X‑adic row soundness and proves its closure under every row operation used by the PM‑basis reduction and completion steps. The file provides a divisibility characterization (rowApproximates_iff), closure lemmas (rowApproximates_rowSub, rowApproximates_rowScaleCoeffX, rowApproximates_cancelKernelLeafLeadingTerm, insertKernelLeafPivotRowWithFuel_approximates, pivotRows_approximates, reduceKernelLeafRowsByPivots_approximates), a lemma for monomial unit rows (rowApproximates_monomialUnitRow), completion lemmas (missingCompletionRows_approximates, completeMissingPivotRows_approximates), and the main composition‑soundness theorem rowApproximates_composed, which states that if a residual‑approximant row is multiplied (via rowMulMatrixWith) by a lower‑approximant basis, the result approximates the original full problem. All proofs are complete; no sorry or admit appear.
CompPoly/LinearAlgebra/PolynomialMatrix/Approximant/PartialLinearization.lean: This new file adds the PartialLinearizationPlan structure and associated helper functions (ceilDivFallback, modulusDegreeMass, chunkDelta, linearizedOrders, principalChunks, principalChunksFromPivotDegrees, etc.) that compute chunk sizes and coordinate offsets for the exact-nullspace lift in diagonal modular-equation solvers. It also provides efficient X-shift utilities (shiftPolynomialX, shiftRowX) and compression operations (compressChunkedPrincipalRow, compressChunkedPrincipalRows) to convert between chunked and principal coordinates. The file defines three constructors for the plan: from a shifted-degree profile, from discovered pivot degrees, and a disabled-chunking variant. No sorry or admit are present.
CompPoly/LinearAlgebra/PolynomialMatrix/MuldersStorjohannCorrectness/Fast.lean: The module-level docstring was reworded to clarify that the fast reducer caches shifted leading positions "once per conflict scan" (instead of "once per scan") and to improve the flow of the description. In the proof of muldersStorjohannReduceWithFuelFast_eq, the anonymous pattern some _ in the cases branch was replaced with a named pattern some pair; this makes the bound variable explicit, though it does not change the logic of the proof.
CompPoly/LinearAlgebra/PolynomialMatrix/MuldersStorjohannCorrectness/Reduction.lean: The file adds a new theorem muldersStorjohannReduceWithFuel_eq_of_no_conflict, which proves that the fueled reducer muldersStorjohannReduceWithFuel is deterministic: if two runs (with possibly different fuel amounts f and g) both produce a matrix with no shifted leading conflict (i.e., shiftedLeadingConflict? returns none), then the two resulting matrices are identical. The proof proceeds by induction on f and case analysis on the presence of a conflict (the hconf case) in shiftedLeadingConflict?, invoking the induction hypothesis when a conflict is resolved via muldersStorjohannStep. This theorem establishes a correctness invariant for the reduction process.
CompPoly/LinearAlgebra/PolynomialMatrix/MuldersStorjohannCorrectness/WeakPopovMinimal.lean: Adds file WeakPopovMinimal.lean with two theorems: shiftedWeakPopov_least_row_minimal proves a predictable-degree property for any shifted weak-Popov matrix – that every row‑span member's shifted degree is bounded below by the shifted degree of some matrix row – without requiring alignment between the shift size and matrix width. muldersStorjohannReduce_least_row_minimal_of_weakPopov re‑derives the least‑row minimality of the Mulders‑Storjohann reducer by invoking the first theorem on the reduced matrix, using existing lemmas about well‑formedness, weak‑Popov preservation, and row‑span equality. The file also publicly re‑exports the Reduction module and contains no sorry or admit declarations.
CompPoly/LinearAlgebra/PolynomialMatrix/Operations.lean: This new file defines reusable polynomial-matrix operations for the CompPoly project. It introduces truncateX and its coefficient lemma truncateX_coeff, the MulLowContext structure for low-product backends, and basic matrix constructors (ofFn, zero, identity, transpose, add, sub, block, joinSquareBlocks). It provides multiplication variants (rowDotWith, rowMulMatrixWith, mulWith, mul, mulTruncXWith, mulLowXWith, mulTruncColumnWith, mulBoundedWith) and a fuel-bounded Strassen-style product (mulStrassenWithFuel, mulStrassenWith) with dimension padding. Additional utilities include coefficient caps (polynomialCoeffCap, productCoeffCap), column truncation (rowTruncateColumns, truncateColumns), modular reduction (modByMonicWith, rowModDiagonalWith, modDiagonalWith), and row selection by shifted degree (leastShiftedDegreeRow?).
CompPoly/LinearAlgebra/PolynomialMatrix/RowSelection.lean: The new file RowSelection.lean defines the predicate RowChoiceValid (a RowChoice is valid if its index is within bounds, its row matches the matrix entry, and its shifted degree is the computed shifted degree) and proves a battery of lemmas about the internal step function leastShiftedDegreeRowStep? and its fold leastShiftedDegreeFold (e.g., leastShiftedDegreeRowStep?_none, leastShiftedDegreeRowStep?_preserves_degree_le, leastShiftedDegreeFold_valid). The three public theorems leastShiftedDegreeChoice?_some_valid, leastShiftedDegreeChoice?_degree_le, and leastShiftedDegreeRow?_some_valid then establish that the high-level leastShiftedDegreeChoice? and leastShiftedDegreeRow? APIs produce correct results: any choice returned is valid, its degree bounds every row's shifted degree, and any row output corresponds to a valid choice. No sorry or admit appear anywhere in the file.
CompPoly/LinearAlgebra/PolynomialMatrix/StrassenCorrectness.lean: The file StrassenCorrectness.lean is newly added (818 lines) and provides the first correctness proofs for the Strassen-style polynomial-matrix products in CompPoly.LinearAlgebra.PolynomialMatrix.Operations. Key theorems include:
rowGet_rowMulMatrixWith and rowMulMatrixWith_size — entry semantics and width of the naive row-by-matrix product.
mulBoundedWith_eq_mulWith — the degree-capped low-product reconstruction equals the naive matrix product.
mulStrassenWithFuel_eq_mulWith and mulStrassenWith_eq_mulWith — the fuel-bounded and unbounded Strassen recursion compute exactly the naive product (as arrays). Consequent lemmas mulStrassenWith_size, mulStrassenWith_getD, matrixRows_mulStrassenWith give size, row access, and row list.
mulTruncColumnStrassenWithFuel_eq_truncateColumns and mulTruncColumnStrassenWith_eq_truncateColumns — the column-truncated Strassen recursion equals the column-truncated naive product. Supporting mulTruncColumnStrassenWith_size and mulTruncColumnStrassenWith_entry give size and entry-level characterisation.
A collection of supporting lemmas: array/fold helpers (getD_of_lt, getD_of_le, foldl_add_eq_sum, etc.), row-access helpers (rowGet_of_size_le, rowGet_list_range_map), truncation algebra (truncateX_zero, truncateX_add, truncateX_sub, truncateX_truncateX, truncateX_sum, truncateX_mul_of_productCoeffCap_le), ofFn access theorems (ofFn_size, getD_ofFn, rowGet_ofFn, MatrixWidth_ofFn, ofFn_congr, etc.), naive product rewrites (mulWith_eq_ofFn, mulWith_size, mulWith_getD, matrixRows_mulWith), Strassen sum identities (four strassen_sum theorems), and padding steps (pad_step, trunc_pad_step).
The public theorem le_nextPowerOfTwoAtLeast (previously private) is now exported.

The file contains no sorry or admit statements – all theorems are fully proved.

ROADMAP.md: Added a roadmap item for the order-basis (approximant) layer over polynomial matrices, which includes modular key equations, a divide-and-conquer PM-Basis recursion with X-adic soundness and kernel-leaf completeness, partial linearization, row selection, minimal weak-Popov forms, and Strassen multiplication used by the recursion.
tests/CompPolyTests.lean: The diff adds a single public import of CompPolyTests.LinearAlgebra.PolynomialMatrix.Approximant to the test file tests/CompPolyTests.lean. This extends the test suite to cover the new PolynomialMatrix.Approximant module, which likely contains tests for polynomial matrix approximants.
tests/CompPolyTests/LinearAlgebra/PolynomialMatrix/Approximant.lean: This new test file adds executable checks for the X-adic approximant problem sizing, PM-basis plumbing, partial-linearization order construction, chunked exact-nullspace lifts, and filtered solution basis extraction. It defines private example data (problem, fullRankProblem, runtime, equation, chunkPlan, profileChunkPlan, discoveredProfile, knownDegreeProblem, knownDegreeRows, productionRows, debugUnchunkedRows, leastChoiceRows) and then uses #guard assertions to verify expected outputs for functions such as maxOrder, totalOrder, lowerOrders, residualOrders, leafDegreeCap, coefficientMatrix, kernelLeafBasis, rowsContainLeadingPosition, missingCompletionRows, mulBoundedWith, mulStrassenWith, mulTruncColumnStrassenWith, pmBasis, MatrixWidth, modulusDegreeMass, chunkDelta, linearizedOrders, chunkedExactNullspaceShift, compressChunkedPrincipalRow, exactNullspaceLift, filterModularSolutionRows, rowSatisfiesModularBool, and leastShiftedDegreeChoice?. No sorry or admit appear; the file provides an executable regression suite for the polynomial-matrix approximant pipeline.

Last updated: 2026-09-02 14:36 UTC.

The linear-algebra half of the Guruswami-Sudan approximant interpolation work from #255, split out so it can be reviewed on its own. It stands under ROADMAP item 10 independently of the decoder backends that consume it. Adds `LinearAlgebra/PolynomialMatrix/Approximant/`: - `ModularEquation/` — modular key equations with soundness and completeness - `PMBasis/` — the divide-and-conquer order-basis recursion, with X-adic soundness, kernel-leaf soundness/completeness, and the scalar and span kernel-leaf layers - `PartialLinearization.lean` — degree balancing for the recursion plus the supporting matrix pieces it needs: `Operations.lean`, `RowSelection.lean`, `StrassenCorrectness.lean` (fast multiplication used by the PM-Basis recursion), and `MuldersStorjohannCorrectness/WeakPopovMinimal.lean`.

Module-system and toolchain adaptation for the relanded order-basis layer. - `import all` for the same-package implementation dependencies these proofs step through (`Univariate.Basic`, `Univariate.Raw.Core`). `coeff`, `ofArray` and the `Raw` wrappers sit in bare `public section`s, so their bodies are opaque downstream and `rw [CPolynomial.ofArray]`, `simp [Raw.coeff]` and `p.coeff i = (↑p).coeff i := rfl` all stopped working. This is the pattern `docs/wiki/module-system.md` prescribes for the case. - `letI` to `let` per the `haveILetI` style linter. - Record the layer under ROADMAP item 10.

dhsorens mentioned this pull request Sep 2, 2026

feat(bivariate): approximant-basis and hybrid GS interpolation #313

Merged

dhsorens changed the base branch from re-land/roots-shoup-lasvegas to main September 2, 2026 14:26

olympichek and others added 2 commits September 2, 2026 15:31

dhsorens force-pushed the restack/pm-approximant branch from c589a82 to 3fec4ad Compare September 2, 2026 14:32

dhsorens mentioned this pull request Sep 2, 2026

feat(bivariate): approximant-basis and hybrid interpolation for GS decoder #255

Closed

dhsorens merged commit 2ee5257 into main Sep 2, 2026
5 checks passed

Navigation Menu

Uh oh!

feat(linalg): order-basis approximant layer over polynomial matrices - #312

feat(linalg): order-basis approximant layer over polynomial matrices#312
dhsorens merged 2 commits into
mainfrom
restack/pm-approximant

dhsorens commented Sep 2, 2026

Uh oh!

github-actions Bot commented Sep 2, 2026 •

edited

Loading

Uh oh!

github-actions Bot commented Sep 2, 2026 •

edited

Loading

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Uh oh!

Conversation

dhsorens commented Sep 2, 2026

Why split

Stack

Contents

Port to current main

Verification

Note

Uh oh!

github-actions Bot commented Sep 2, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Build Timing Report

Incremental Rebuild Signal

Slowest Current Build Files (warm library build)

Uh oh!

github-actions Bot commented Sep 2, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

🤖 PR Summary

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

github-actions Bot commented Sep 2, 2026 •

edited

Loading

github-actions Bot commented Sep 2, 2026 •

edited

Loading