Diagonal Modular Equations #
GS-independent solution-basis interface for systems
p * matrix = 0 mod diag(moduli).
The production solver follows the degree-first pattern: it solves chunked
exact-nullspace X-adic problems whose partial-linearization windows are grown
adaptively per principal coordinate, doubling only the windows of coordinates
whose shifted pivot degree has not been discovered yet. Because a window stops
growing once its coordinate's pivot is found, the total window mass stays
within a constant factor of the true pivot-degree mass, which is at most the
modulus degree mass sigma. Every round is therefore an X-adic problem with
O(m) chunk rows and total order O(sigma), and the number of rounds is
logarithmic, preserving the ~O(m^(omega-1) * sigma) solver target.
The chunked X-adic problems are relaxations: their orders certify exactness
only for rows whose chunk coefficients stay below the chunk size, and the
relaxed kernel module also contains uncertified rows that can crowd exact
solutions out of the adaptive rounds. The solver therefore backs the adaptive
loop with a certified verification solve (windowedSolutionBasisViaPMBasis):
solutions at or above the adaptive best are dominated by the adaptive rows,
and solutions below it lie inside the certified window, whose orders rule out
uncertified rows.
Callers that only need a witness under a known degree bound pass it as
degreeBound?; when the adaptive best already meets the bound the certified
solve is skipped entirely, and when it does not the certified window is shrunk
to the bound. Passing none requests a degree-minimal answer and always runs
the verification solve over the best-degree-shrunk window.
References #
- [Giorgi, P., Jeannerod, C.-P., and Villard, G., On the complexity of polynomial matrix computations][GJV03]
- [Storjohann, A., Notes on computing minimal approximant bases][Sto06]
- [Chowdhury, M. F. I., Jeannerod, C.-P., Neiger, V., Schost, E., and Villard, G., Faster algorithms for multivariate interpolation with multiplicities and simultaneous polynomial approximations][CJNSV15]
Diagonal modular-equation data. Rows of matrix are solution coordinates;
columns are reduced independently by moduli.
- moduli : Array (CPolynomial F)
- matrix : PolynomialMatrix F
Instances For
Number of principal solution coordinates.
Instances For
Number of modular columns.
Instances For
Diagonal rows -diag(moduli) for the exact-nullspace lift.
Instances For
Exact-nullspace lift [F; -diag(M)].
Instances For
Principal solution rows: keep the first solutionWidth entries of each
expanded nullspace row.
Instances For
Build the X-adic exact-nullspace problem used by the modular-equation solver.
Instances For
Entry-aware X-adic orders for a chunked exact-nullspace lift. A balanced
in-window solution has chunk coefficients of degree below delta, and the
chunked principal entries of column b are reduced below deg M_b, so
delta + maxEntryDeg + 1 low coefficients certify that its principal product
vanishes exactly. This is never larger than the generic
deg M_b + delta + 1 order and is much smaller when the relation entries have
low degree.
Instances For
Principal rows for the chunked exact-nullspace lift. Chunk row
(coord, offset) stores X^offset times the corresponding original relation
row, reduced columnwise by the diagonal moduli. Reducing keeps every entry of
column b below deg M_b, matching the E * F mod M expansion from the
design notes and keeping chunked entry degrees independent of the offsets.
Instances For
Chunked exact-nullspace lift for a partial-linearization plan.
Instances For
Build the X-adic exact-nullspace problem after principal-coordinate chunk expansion, with generic partial-linearization orders.
Instances For
Build the chunked X-adic exact-nullspace problem with entry-aware orders.
The shift argument is kept for call-site symmetry; orders depend only on the
chunked entry degrees and the chunk size.
Instances For
Shifted pivot-degree profile discovered for the principal solution
coordinates. none means that the discovery pass did not see a row pivoting in
that coordinate, so partial linearization uses its conservative fallback.
Instances For
Empty shifted pivot-degree profile for a fixed principal width.
Instances For
Insert a discovered pivot degree, keeping the smallest degree for each principal leading position.
Instances For
Whether the profile has discovered a pivot degree for every coordinate.
Instances For
Whether the profile has discovered a pivot degree for any coordinate.
Instances For
Merge the principal pivot degrees observed in rows into a profile.
Instances For
Discover principal pivot degrees from compressed candidate rows.
Instances For
Solve a diagonal modular equation with a supplied partial-linearization plan.
Instances For
Solve once with the conservative shift-spread window. This is a debug entry point only: its chunk count can grow quadratically in the module width for spread-out shifts, so the production solver uses the adaptive window-escalation loop instead.
Instances For
Known-degree reconstruction pass: build the partial-linearization plan from the discovered pivot degrees and solve the X-adic problem directly for that profile.
Instances For
Solve once without principal-coordinate chunking. This is an explicit tiny-leaf/debug entry point; the default modular-equation context does not use it as a production fallback.
Instances For
Keep only rows that satisfy the original diagonal modular equation after compression from the exact-nullspace / X-adic bridge.
Instances For
Residual rows B * F mod diag(M) for candidate solution rows B.
Instances For
Shift used for polynomial combinations of compressed candidate rows. The
degree of a coefficient multiplying row i is measured relative to the shifted
degree already carried by that candidate row.
Instances For
Upper bound for the adaptive search window above each coordinate's shift.
The row e_j * lcm(moduli) is always a solution and deg lcm(moduli) is at
most the modulus degree mass, so every coordinate's minimal shifted pivot
degree is within this window.
Instances For
Coefficient-degree bound for the full-window fallback problem. Any row of
the lifted module whose shifted degree does not exceed the shifted degree of an
in-window solution has plain coefficient degrees at most
pivotWindowCap + maxShiftDegree shift: comparing two principal coordinates
costs at most the shift spread, and pivotWindowCap bounds every minimal
pivot degree.
Instances For
Exact-nullspace lift with the relation entries reduced columnwise by the
moduli, so every principal entry of column b has degree below deg M_b and
the quotient coefficients of exact solutions stay below the solution degree.
Instances For
Unchunked exact-nullspace problem with orders certifying exactness across
the whole pivot window: a lifted row with principal coefficient degrees at most
bound and quotient coefficient degrees at most bound + 1 produces column-b
products of degree below deg M_b + bound + 2, so vanishing to that X-adic
order forces the product to vanish exactly. Unlike the chunked relaxation,
this problem admits no uncertified rows below the in-window solution degrees,
at the cost of an order mass larger by a factor of the module width.
Instances For
Certified full-window solve: compute a minimal basis of the unchunked exact-nullspace problem whose orders cover the entire pivot window, and keep the principal columns. Every returned row that pivots at or below an in-window solution degree is an exact modular solution, so this entry point cannot lose the solution basis to uncertified low-degree rows. It is used as the fallback when the chunked adaptive solver discovers nothing.
Instances For
Certified verification window sized by the best exact degree already in hand. Solutions at or above the best adaptive degree are dominated by the adaptive result itself, so the certified window only has to cover the degrees strictly below it; when the adaptive loop found nothing it falls back to the full pivot window.
Instances For
Certified solve over an explicit coefficient-degree window: an unchunked
exact-nullspace problem whose orders certify exactness for every row dominated
by an in-window solution. Its order mass is sigma + s * bound instead of
the full window's (s + 1) * sigma, so when the window is shrunk to a
near-minimal degree this costs about one extra cheap round.
Instances For
Certified verification solve over the best-degree-shrunk window sized by
verificationWindowBound.
Instances For
Whether a caller-supplied degree bound certifies the adaptive result: the gate passes when the best exact degree already found does not exceed the bound, in which case any solution within the bound is dominated by the adaptive rows up to the bound itself and the certified verification solve is unnecessary.
Instances For
Verification window for a gated solve. With a caller-supplied degree
bound the window only has to cover solutions within the bound, so it is
min(bound, cap) + maxShift; without one it falls back to the best-degree
window of verificationWindowBound.
Instances For
The degree gate passes exactly for a bound certified by an adaptive best.
Pivot-degree assignment for one adaptive round: discovered coordinates use their observed pivot degrees, undiscovered coordinates use the current escalation window above their shift entry.
Instances For
Least shifted degree among accumulated solution rows.
Instances For
A coordinate needs no wider search window once its pivot degree is
discovered, its window has reached the cap, or its window already covers every
degree below the best solution row found so far. The last rule is what keeps
the loop from growing windows for coordinates that cannot improve the answer:
a row pivoting at j with shifted degree below the current best would lie
inside the already-searched window. Improving on best needs a row of degree
at most best - 1, so the window shift[j] + budget[j] suffices once
best <= shift[j] + budget[j] + 1.
Instances For
Double the escalation windows of coordinates that are not settled, clamped at the window cap. Settled coordinates keep their window so the total window mass stays within a constant factor of the useful pivot-degree mass.
Instances For
State carried between adaptive solution-basis rounds. filtered
accumulates the exact solution rows found across all rounds.
- profile : PivotDegreeProfile
- filtered : PolynomialMatrix F
- raw : PolynomialMatrix F
Instances For
One adaptive round: solve the chunked exact-nullspace problem for the current window assignment, keep the rows that satisfy the original diagonal congruences, and merge the observed shifted pivot degrees into the profile.
Instances For
Fuel-bounded adaptive window-escalation loop. Rounds stop as soon as the caller's degree bound is already met by the best exact row found, or every principal coordinate is settled: discovered, saturated, or unable to beat the best solution row already in hand.
Instances For
Run the adaptive degree-first solver: discover the shifted pivot-degree profile with geometrically growing per-coordinate windows, where the final round doubles as the known-degree reconstruction for all discovered coordinates. The initial window is one chunk per coordinate. A caller with a degree bound stops the escalation as soon as the bound is met.
Instances For
Discover the shifted pivot-degree profile through the adaptive solver.
Instances For
One residual reconstruction pass. If compressed rows B are not themselves
exact modular solutions, solve for polynomial combinations C such that
C * (B * F mod M) = 0 mod M, then return C * B. The residual equation is
solved with the same adaptive solver, without a further repair recursion.
The candidate rows are first reduced to one representative per shifted leading position. The reduction steps are unimodular, so the generated row module is unchanged, while the residual equation's solution width stays bounded by the principal width instead of the raw candidate count; without this bound the repair solve can be quadratically wider than the original equation.
Instances For
Debug helper for tiny problems that intentionally disables principal-coordinate chunking, keeping an unchunked solve available for inspection without letting the production context bypass partial linearization.
Instances For
Known-degree reconstruction followed by the original diagonal-equation guard. The reconstruction plan is built from discovered shifted pivot degrees, solved as a chunked exact-nullspace PM-basis problem, and compressed back to the principal solution coordinates.
Instances For
Solver exposed through the modular-equation context: run the adaptive
degree-first window-escalation loop, whose final round is the known-degree
reconstruction for every discovered coordinate, then back it with a certified
verification solve. When the caller supplies a degree bound and the best
exact degree already found meets it, the adaptive candidate set is returned
as-is: any solution within the bound is then matched by an adaptive row up to
the bound, so the certified solve adds nothing the caller can observe.
Otherwise a certified verification solve runs over the gated window —
min(bound, cap) + maxShift with a bound, the best-degree-shrunk window
without one — and the union of both filtered candidate sets is returned:
solutions at or above the adaptive best are dominated by the adaptive rows;
solutions strictly below it lie inside the certified window, whose orders rule
out uncertified relaxed rows — so the union always contains an exact row of
minimal shifted degree, including in the partial-masking regime where
uncertified chunked-kernel rows crowd lower exact solutions out of every
adaptive round. The adaptive rows come first, so ties keep the adaptive
choice. The residual repair pass remains as a guard when both candidate sets
are empty. The filter, verification, and repair are semantic guards around
the exact-nullspace bridge; they do not call any alternate interpolation
backend.
Instances For
Rows kept by the modular solution filter satisfy the modular predicate.
One adaptive round preserves modular soundness of the accumulated filtered rows.
The adaptive escalation loop preserves modular soundness of the accumulated filtered rows.
Rows accumulated by the adaptive solver satisfy the modular predicate.
Every row returned by the filtered PM-basis modular solver satisfies the original diagonal modular equation.
Modular-equation solution-basis context with theorem fields.
The solver takes an optional caller-supplied degree bound. The
completeness/minimality contract is bound-relative: for any nonzero in-width
solution row of the diagonal modular equation whose shifted degree fits the
bound (vacuous for none), the returned basis stays inside the principal
width and contains a row whose shifted degree does not exceed the bound — the
given solution's own degree when no bound is supplied. The contract assumes
monic moduli, a relation matrix wide enough to expose every modular column to
the executable row predicate, and a shift aligned with the principal solution
width.
- mulContext : CPolynomial.MulContext F
- modContext : CPolynomial.ModContext F
- solutionBasis : ModularEquation F → Array ℕ → Option ℕ → PolynomialMatrix F
- sound (equation : ModularEquation F) (shift : Array ℕ) (degreeBound? : Option ℕ) (row : PolynomialRow F) : row ∈ (self.solutionBasis equation shift degreeBound?).MatrixRows → rowSatisfiesModularBool self.mulContext self.modContext row equation.matrix equation.moduli = true
- complete_minimal (equation : ModularEquation F) (shift : Array ℕ) (degreeBound? : Option ℕ) (row : PolynomialRow F) (rowDegree : ℕ) : (∀ b < equation.moduli.size, (equation.moduli.getD b 0).monic = true) → equation.moduli.size ≤ equation.matrix.MatrixWidth → shift.size = equation.solutionWidth → rowSatisfiesModularBool self.mulContext self.modContext row equation.matrix equation.moduli = true → rowIsZero row = false → Array.size row ≤ equation.solutionWidth → rowShiftedDegree? row shift = some rowDegree → (∀ (bound : ℕ), degreeBound? = some bound → rowDegree ≤ bound) → (∀ basisRow ∈ (self.solutionBasis equation shift degreeBound?).MatrixRows, Array.size basisRow ≤ equation.solutionWidth) ∧ ∃ (basisRow : PolynomialRow F) (degree : ℕ), basisRow ∈ (self.solutionBasis equation shift degreeBound?).MatrixRows ∧ rowShiftedDegree? basisRow shift = some degree ∧ degree ≤ degreeBound?.getD rowDegree