Polynomial-Matrix Operations

Reusable executable operations for polynomial rows and row-major polynomial matrices. The multiplication and reduction entry points take explicit univariate operation contexts so concrete fields can supply fast polynomial arithmetic.

def CompPoly.PolynomialMatrix.truncateX {F : Type u_1} [Zero F] [BEq F] [LawfulBEq F] (order : ℕ) (p : CPolynomial F) : CPolynomial F

Keep the coefficients of degree < order.

theorem CompPoly.PolynomialMatrix.truncateX_coeff {F : Type u_1} [Semiring F] [BEq F] [LawfulBEq F] (order : ℕ) (p : CPolynomial F) (i : ℕ) : (truncateX order p).coeff i = if i < order then p.coeff i else 0

Coefficients of an X-adic truncation.

structure CompPoly.PolynomialMatrix.MulLowContext (F : Type u_2) [Semiring F] [BEq F] [LawfulBEq F] : Type u_2

Polynomial-matrix low-product backend. The full multiplication context is kept beside the low-product operation because recursive PM-basis still needs ordinary basis composition.

• mulContext : CPolynomial.MulContext F
• mulLow : ℕ → CPolynomial F → CPolynomial F → CPolynomial F
• mulLow_eq (order : ℕ) (p q : CPolynomial F) : self.mulLow order p q = truncateX order (p * q)

  The backend returns exactly the truncated canonical product.

def CompPoly.PolynomialMatrix.MulLowContext.fromMulContext {F : Type u_1} [Semiring F] [BEq F] [LawfulBEq F] (mulCtx : CPolynomial.MulContext F) : MulLowContext F

Low-product backend obtained by truncating a full univariate product.

def CompPoly.PolynomialMatrix.MulLowContext.raw {F : Type u_1} [Semiring F] [BEq F] [LawfulBEq F] (mulCtx : CPolynomial.MulContext F) (rawCtx : CPolynomial.Raw.MulLowContext F) : MulLowContext F

Low-product backend backed directly by a raw low-product implementation.

def CompPoly.PolynomialMatrix.ofFn {F : Type u_1} [Zero F] (rows width : ℕ) (entry : ℕ → ℕ → CPolynomial F) : PolynomialMatrix F

Build a row-major polynomial matrix from an indexed entry function.

def CompPoly.PolynomialMatrix.zero {F : Type u_1} [Zero F] (rows width : ℕ) : PolynomialMatrix F

The zero matrix of a fixed shape.

def CompPoly.PolynomialMatrix.identity {F : Type u_1} [Semiring F] [BEq F] [LawfulBEq F] [Nontrivial F] (n : ℕ) : PolynomialMatrix F

The polynomial identity matrix of size n.

def CompPoly.PolynomialMatrix.transpose {F : Type u_1} [Zero F] (M : PolynomialMatrix F) : PolynomialMatrix F

Matrix transpose, using zero defaults for ragged input rows.

def CompPoly.PolynomialMatrix.rowDotWith {F : Type u_1} [Semiring F] [BEq F] [LawfulBEq F] (mulCtx : CPolynomial.MulContext F) (a b : PolynomialRow F) : CPolynomial F

Dot product of two polynomial rows using an explicit univariate multiplication context.

def CompPoly.PolynomialMatrix.rowMulMatrixWith {F : Type u_1} [Semiring F] [BEq F] [LawfulBEq F] (mulCtx : CPolynomial.MulContext F) (row : PolynomialRow F) (M : PolynomialMatrix F) : PolynomialRow F

Row-by-matrix product using an explicit univariate multiplication context.

def CompPoly.PolynomialMatrix.mulWith {F : Type u_1} [Semiring F] [BEq F] [LawfulBEq F] (mulCtx : CPolynomial.MulContext F) (A B : PolynomialMatrix F) : PolynomialMatrix F

Matrix product using an explicit univariate multiplication context.

def CompPoly.PolynomialMatrix.mul {F : Type u_1} [Semiring F] [BEq F] [LawfulBEq F] (A B : PolynomialMatrix F) : PolynomialMatrix F

Matrix product backed by canonical univariate multiplication.

def CompPoly.PolynomialMatrix.add {F : Type u_1} [Semiring F] [BEq F] [LawfulBEq F] (A B : PolynomialMatrix F) : PolynomialMatrix F

Pointwise matrix addition, using zero defaults for ragged inputs.

def CompPoly.PolynomialMatrix.sub {F : Type u_1} [Ring F] [BEq F] [LawfulBEq F] (A B : PolynomialMatrix F) : PolynomialMatrix F

Pointwise matrix subtraction, using zero defaults for ragged inputs.

def CompPoly.PolynomialMatrix.block {F : Type u_1} [Zero F] (M : PolynomialMatrix F) (rowStart rowCount colStart colCount : ℕ) : PolynomialMatrix F

Extract a rectangular block with zero defaults for out-of-range entries.

def CompPoly.PolynomialMatrix.joinSquareBlocks {F : Type u_1} [Zero F] (half : ℕ) (C₁₁ C₁₂ C₂₁ C₂₂ : PolynomialMatrix F) : PolynomialMatrix F

Join four equally sized square blocks into one square matrix.

def CompPoly.PolynomialMatrix.nextPowerOfTwoAtLeastLoop (target : ℕ) : ℕ → ℕ → ℕ

Fuel-bounded doubling loop for the smallest power of two at least target.

def CompPoly.PolynomialMatrix.nextPowerOfTwoAtLeast (target : ℕ) : ℕ

Smallest power of two at least target, with 1 returned for 0.

def CompPoly.PolynomialMatrix.multiplicationDimension {F : Type u_1} [Zero F] (A B : PolynomialMatrix F) : ℕ

Runtime dimension controlling rectangular polynomial-matrix multiplication.

def CompPoly.PolynomialMatrix.padSquare {F : Type u_1} [Zero F] (n : ℕ) (M : PolynomialMatrix F) : PolynomialMatrix F

Pad a matrix to an n × n square using the zero-default block extractor.

def CompPoly.PolynomialMatrix.trimShape {F : Type u_1} [Zero F] (rows width : ℕ) (M : PolynomialMatrix F) : PolynomialMatrix F

Trim a matrix to a rectangular output shape.

def CompPoly.PolynomialMatrix.natArraySlice (values : Array ℕ) (start count : ℕ) : Array ℕ

Slice count natural-number entries, using zero defaults out of bounds.

def CompPoly.PolynomialMatrix.maxNatArrays (a b : Array ℕ) : Array ℕ

Pointwise maximum of two natural-number arrays.

def CompPoly.PolynomialMatrix.polynomialCoeffCap {F : Type u_1} [Zero F] [BEq F] (p : CPolynomial F) : ℕ

Number of coefficients needed to represent a polynomial exactly.

def CompPoly.PolynomialMatrix.productCoeffCap {F : Type u_1} [Zero F] [BEq F] (p q : CPolynomial F) : ℕ

Number of low coefficients sufficient for one product term exactly.

def CompPoly.PolynomialMatrix.rowMulMatrixEntryCoeffCap {F : Type u_1} [Zero F] [BEq F] (row : PolynomialRow F) (M : PolynomialMatrix F) (j : ℕ) : ℕ

Per-entry coefficient cap for one row-by-matrix product entry.

def CompPoly.PolynomialMatrix.rowTruncateColumns {F : Type u_1} [Zero F] [BEq F] [LawfulBEq F] (orders : Array ℕ) (row : PolynomialRow F) : PolynomialRow F

Truncate one row with independent output-column orders.

def CompPoly.PolynomialMatrix.truncateColumns {F : Type u_1} [Zero F] [BEq F] [LawfulBEq F] (orders : Array ℕ) (M : PolynomialMatrix F) : PolynomialMatrix F

Truncate a matrix with independent output-column orders.

def CompPoly.PolynomialMatrix.mulTruncXWith {F : Type u_1} [Semiring F] [BEq F] [LawfulBEq F] (mulCtx : CPolynomial.MulContext F) (order : ℕ) (p q : CPolynomial F) : CPolynomial F

Multiply and retain only coefficients of degree < order.

def CompPoly.PolynomialMatrix.mulLowXWith {F : Type u_1} [Semiring F] [BEq F] [LawfulBEq F] (lowCtx : MulLowContext F) (order : ℕ) (p q : CPolynomial F) : CPolynomial F

Low-product entry point for the first order coefficients.

def CompPoly.PolynomialMatrix.divXTrunc {F : Type u_1} [Zero F] [BEq F] [LawfulBEq F] (shift order : ℕ) (p : CPolynomial F) : CPolynomial F

Divide by X^shift and keep order coefficients.

def CompPoly.PolynomialMatrix.modByMonicWith {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (modCtx : CPolynomial.ModContext F) (p modulus : CPolynomial F) : CPolynomial F

Reduce by a monic modulus when one is present. A zero modulus is treated as an absent modulus and leaves the input unchanged.

def CompPoly.PolynomialMatrix.rowModDiagonalWith {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (modCtx : CPolynomial.ModContext F) (moduli : Array (CPolynomial F)) (row : PolynomialRow F) : PolynomialRow F

Reduce a row by independent diagonal moduli. The output width is the number of supplied moduli.

def CompPoly.PolynomialMatrix.modDiagonalWith {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (modCtx : CPolynomial.ModContext F) (moduli : Array (CPolynomial F)) (M : PolynomialMatrix F) : PolynomialMatrix F

Reduce every matrix row by independent diagonal moduli.

def CompPoly.PolynomialMatrix.rowMulMatrixModDiagonalWith {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (mulCtx : CPolynomial.MulContext F) (modCtx : CPolynomial.ModContext F) (row : PolynomialRow F) (M : PolynomialMatrix F) (moduli : Array (CPolynomial F)) : PolynomialRow F

Row-by-matrix product followed by diagonal modular reduction.

def CompPoly.PolynomialMatrix.rowMulMatrixTruncColumnWith {F : Type u_1} [Semiring F] [BEq F] [LawfulBEq F] (lowCtx : MulLowContext F) (orders : Array ℕ) (row : PolynomialRow F) (M : PolynomialMatrix F) : PolynomialRow F

Row-by-matrix product with independent output-column truncation. Column j keeps coefficients of degree < orders[j]; this is the residual-window primitive used by recursive PM-basis.

def CompPoly.PolynomialMatrix.mulTruncColumnWith {F : Type u_1} [Semiring F] [BEq F] [LawfulBEq F] (lowCtx : MulLowContext F) (orders : Array ℕ) (A B : PolynomialMatrix F) : PolynomialMatrix F

Matrix product with independent output-column truncation.

def CompPoly.PolynomialMatrix.mulTruncColumnStrassenWithFuel {F : Type u_1} [Ring F] [BEq F] [LawfulBEq F] (lowCtx : MulLowContext F) (leafCutoff : ℕ) : ℕ → Array ℕ → PolynomialMatrix F → PolynomialMatrix F → PolynomialMatrix F

Fuel-bounded Strassen-style matrix product with independent output-column truncation orders.

def CompPoly.PolynomialMatrix.mulTruncColumnStrassenWith {F : Type u_1} [Ring F] [BEq F] [LawfulBEq F] (lowCtx : MulLowContext F) (leafCutoff : ℕ) (orders : Array ℕ) (A B : PolynomialMatrix F) : PolynomialMatrix F

Strassen-style matrix product with independent output-column truncation orders and conservative default fuel.

def CompPoly.PolynomialMatrix.rowMulMatrixBoundedWith {F : Type u_1} [Semiring F] [BEq F] [LawfulBEq F] (lowCtx : MulLowContext F) (row : PolynomialRow F) (M : PolynomialMatrix F) : PolynomialRow F

Row-by-matrix product with per-output-entry degree caps inferred from input degree profiles. This reconstructs the exact row product while routing every term through low-product multiplication.

def CompPoly.PolynomialMatrix.mulBoundedWith {F : Type u_1} [Semiring F] [BEq F] [LawfulBEq F] (lowCtx : MulLowContext F) (A B : PolynomialMatrix F) : PolynomialMatrix F

Matrix product reconstructed from inferred per-entry degree caps. Recursive composition uses this only as its small-leaf and fuel-exhausted fallback.

def CompPoly.PolynomialMatrix.mulStrassenWithFuel {F : Type u_1} [Ring F] [BEq F] [LawfulBEq F] (lowCtx : MulLowContext F) (leafCutoff : ℕ) : ℕ → PolynomialMatrix F → PolynomialMatrix F → PolynomialMatrix F

Fuel-bounded Strassen-style matrix product.

Small inputs and exhausted fuel use the bounded row-column product. Larger rectangular or odd-sized inputs are padded to square power-of-two shape, routed through the recursive block product, and trimmed back to the requested output shape.

def CompPoly.PolynomialMatrix.mulStrassenWith {F : Type u_1} [Ring F] [BEq F] [LawfulBEq F] (lowCtx : MulLowContext F) (leafCutoff : ℕ) (A B : PolynomialMatrix F) : PolynomialMatrix F

Strassen-style matrix product with a conservative default fuel.

def CompPoly.PolynomialMatrix.rowSatisfiesModularBool {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (mulCtx : CPolynomial.MulContext F) (modCtx : CPolynomial.ModContext F) (row : PolynomialRow F) (M : PolynomialMatrix F) (moduli : Array (CPolynomial F)) : Bool

Executable modular-equation row predicate.

def CompPoly.PolynomialMatrix.shiftedRowDegreeProfile {F : Type u_1} [Zero F] [BEq F] (M : PolynomialMatrix F) (shift : Array ℕ) : Array (Option ℕ)

Shifted row-degree profile for all rows.

structure CompPoly.PolynomialMatrix.RowChoice (F : Type u_2) [Zero F] : Type u_2

Candidate row selected by least-shifted-degree scanning.

• index : ℕ
• row : PolynomialRow F
• degree : ℕ

def CompPoly.PolynomialMatrix.betterRowChoice {F : Type u_1} [Zero F] (candidate current : RowChoice F) : Bool

Tie-breaking order for least-shifted-degree row selection.

def CompPoly.PolynomialMatrix.leastShiftedDegreeRowStep? {F : Type u_1} [Zero F] [BEq F] (M : PolynomialMatrix F) (shift : Array ℕ) (best : Option (RowChoice F)) (i : ℕ) : Option (RowChoice F)

One left-to-right scan step for least-shifted-degree row selection.

def CompPoly.PolynomialMatrix.leastShiftedDegreeChoice? {F : Type u_1} [Zero F] [BEq F] (M : PolynomialMatrix F) (shift : Array ℕ) : Option (RowChoice F)

Scan row indices for the best least-shifted-degree candidate.

def CompPoly.PolynomialMatrix.leastShiftedDegreeRow? {F : Type u_1} [Zero F] [BEq F] (M : PolynomialMatrix F) (shift : Array ℕ) : Option (PolynomialRow F)

Select a nonzero row of least shifted degree.