Partial-Linearization Parameters

Small executable helpers used by diagonal modular-equation solvers to size the expanded X-adic problem without using one global oversized order.

References

• [Storjohann, A., Notes on computing minimal approximant bases][Sto06]

def CompPoly.PolynomialMatrix.Approximant.ceilDivFallback (n d : ℕ) : ℕ

Ceiling division with 1 as the zero-width fallback.

def CompPoly.PolynomialMatrix.Approximant.modulusDegreeMass {F : Type u_1} [Zero F] (moduli : Array (CPolynomial F)) : ℕ

Degree mass of diagonal moduli.

def CompPoly.PolynomialMatrix.Approximant.chunkDelta {F : Type u_1} [Zero F] (solutionWidth : ℕ) (moduli : Array (CPolynomial F)) : ℕ

Chunk size Delta = ceil(sigma / m) used for partial linearization.

def CompPoly.PolynomialMatrix.Approximant.linearizedOrders {F : Type u_1} [Zero F] (solutionWidth : ℕ) (moduli : Array (CPolynomial F)) : Array ℕ

X-adic orders for the exact-nullspace lift, using the local chunk size.

def CompPoly.PolynomialMatrix.Approximant.maxShiftDegree (shift : Array ℕ) : ℕ

Maximum shifted-degree offset in a principal-coordinate shift.

def CompPoly.PolynomialMatrix.Approximant.principalShiftOffset (_shift : Array ℕ) (delta : ℕ) : ℕ

Offset added to every principal coordinate when lifting to exact-nullspace coordinates. Adding the same positive offset to every principal coordinate preserves their relative shifted degrees; quotient coordinates are shifted separately above the principal search window.

def CompPoly.PolynomialMatrix.Approximant.quotientShift (_shift : Array ℕ) (delta : ℕ) : ℕ

Quotient-coordinate shift used by the exact-nullspace lift. It is kept at the chunk degree so quotient coordinates do not dominate the shifted degree of principal relation rows. Rows that compress to zero are removed later by the principal-row filter.

def CompPoly.PolynomialMatrix.Approximant.liftedPrincipalShift (shift : Array ℕ) (delta : ℕ) : Array ℕ

Principal-coordinate shift used inside the exact-nullspace lift.

def CompPoly.PolynomialMatrix.Approximant.exactNullspaceShift (shift : Array ℕ) (quotientWidth delta : ℕ) : Array ℕ

Extend the principal solution shift with low quotient shifts.

structure CompPoly.PolynomialMatrix.Approximant.PrincipalChunk : Type

One chunk of a principal solution coordinate. It represents X^offset * chunkPoly in coordinate coord.

• coord : ℕ
• offset : ℕ

@[instance_reducible]

instance CompPoly.PolynomialMatrix.Approximant.instReprPrincipalChunk : Repr PrincipalChunk

def CompPoly.PolynomialMatrix.Approximant.instReprPrincipalChunk.repr : PrincipalChunk → ℕ → Std.Format

@[instance_reducible]

instance CompPoly.PolynomialMatrix.Approximant.instBEqPrincipalChunk : BEq PrincipalChunk

def CompPoly.PolynomialMatrix.Approximant.instBEqPrincipalChunk.beq : PrincipalChunk → PrincipalChunk → Bool

@[instance_reducible]

instance CompPoly.PolynomialMatrix.Approximant.instDecidableEqPrincipalChunk : DecidableEq PrincipalChunk

def CompPoly.PolynomialMatrix.Approximant.instDecidableEqPrincipalChunk.decEq (x✝ x✝¹ : PrincipalChunk) : Decidable (x✝ = x✝¹)

def CompPoly.PolynomialMatrix.Approximant.principalChunkCount (solutionWidth : ℕ) (shift : Array ℕ) (delta j : ℕ) : ℕ

Number of chunks used for one principal coordinate from a shifted-degree profile.

def CompPoly.PolynomialMatrix.Approximant.principalChunks (solutionWidth : ℕ) (shift : Array ℕ) (delta : ℕ) : Array PrincipalChunk

Principal chunks induced by the known shifted-degree profile.

def CompPoly.PolynomialMatrix.Approximant.principalUnitChunks (solutionWidth : ℕ) : Array PrincipalChunk

One unshifted chunk for each principal coordinate.

def CompPoly.PolynomialMatrix.Approximant.fallbackPivotDegree (solutionWidth : ℕ) (shift : Array ℕ) : ℕ

Fallback shifted pivot degree used before discovery has produced a degree for one coordinate.

def CompPoly.PolynomialMatrix.Approximant.pivotDegreeAt (solutionWidth : ℕ) (shift : Array ℕ) (pivotDegrees : Array (Option ℕ)) (j : ℕ) : ℕ

Pivot degree for one coordinate, falling back to the shift spread when the profile has not discovered that coordinate.

def CompPoly.PolynomialMatrix.Approximant.principalChunkCountFromPivotDegree (shift : Array ℕ) (delta j pivotDegree : ℕ) : ℕ

Number of chunks for one principal coordinate from a discovered shifted pivot-degree profile.

def CompPoly.PolynomialMatrix.Approximant.principalChunksFromPivotDegrees (solutionWidth : ℕ) (shift : Array ℕ) (delta : ℕ) (pivotDegrees : Array (Option ℕ)) : Array PrincipalChunk

Principal chunks induced by a discovered shifted pivot-degree profile.

structure CompPoly.PolynomialMatrix.Approximant.PartialLinearizationPlan : Type

Executable partial-linearization plan for the exact-nullspace lift.

• solutionWidth : ℕ
• quotientWidth : ℕ
• delta : ℕ
• chunks : Array PrincipalChunk

def CompPoly.PolynomialMatrix.Approximant.partialLinearizationPlan {F : Type u_1} [Zero F] (solutionWidth quotientWidth : ℕ) (moduli : Array (CPolynomial F)) (shift : Array ℕ) : PartialLinearizationPlan

Build a chunk plan from the modular shape and shifted-degree profile.

def CompPoly.PolynomialMatrix.Approximant.partialLinearizationPlanFromPivotDegrees {F : Type u_1} [Zero F] (solutionWidth quotientWidth : ℕ) (moduli : Array (CPolynomial F)) (shift : Array ℕ) (pivotDegrees : Array (Option ℕ)) : PartialLinearizationPlan

Build a chunk plan from a discovered shifted pivot-degree profile.

def CompPoly.PolynomialMatrix.Approximant.unchunkedPartialLinearizationPlan {F : Type u_1} [Zero F] (solutionWidth quotientWidth : ℕ) (moduli : Array (CPolynomial F)) : PartialLinearizationPlan

Plan with partial linearization disabled for the principal coordinates.

def CompPoly.PolynomialMatrix.Approximant.xPowPolynomial {F : Type u_1} [Zero F] [One F] [BEq F] [LawfulBEq F] (offset : ℕ) : CPolynomial F

Monomial X^offset as a canonical polynomial, built without requiring the CPolynomial.X nontriviality instance.

def CompPoly.PolynomialMatrix.Approximant.shiftPolynomialX {F : Type u_1} [Semiring F] [BEq F] [LawfulBEq F] (offset : ℕ) (p : CPolynomial F) : CPolynomial F

Multiply a polynomial by X^offset by shifting its coefficient array. This is an O(offset + deg p) array operation; it must not go through generic polynomial multiplication, which would cost O(offset * deg p).

def CompPoly.PolynomialMatrix.Approximant.shiftRowX {F : Type u_1} [Semiring F] [BEq F] [LawfulBEq F] (offset : ℕ) (row : PolynomialRow F) : PolynomialRow F

Shift every entry of a row by X^offset.

def CompPoly.PolynomialMatrix.Approximant.chunkedExactNullspaceShift (plan : PartialLinearizationPlan) (shift : Array ℕ) : Array ℕ

Shift for the chunked exact-nullspace problem.

def CompPoly.PolynomialMatrix.Approximant.compressChunkedPrincipalRow {F : Type u_1} [Semiring F] [BEq F] [LawfulBEq F] (plan : PartialLinearizationPlan) (row : PolynomialRow F) : PolynomialRow F

Compress one row in chunked coordinates back to the principal solution coordinates.

def CompPoly.PolynomialMatrix.Approximant.compressChunkedPrincipalRows {F : Type u_1} [Semiring F] [BEq F] [LawfulBEq F] (plan : PartialLinearizationPlan) (basis : PolynomialMatrix F) : PolynomialMatrix F

Compress every row in a chunked basis back to the principal coordinates.