Scalar Kernel-Leaf PM-Basis Definitions

Executable definitions for the classical scalar-kernel PM-basis leaf: the dense coefficient matrix and its row-array RREF kernel, reconstruction of polynomial rows from kernel vectors, monomial completion rows, and the shifted pivot-table reduction used to compact leaf bases.

def CompPoly.PolynomialMatrix.Approximant.leafDegreeCap {F : Type u_1} [Field F] (problem : XAdicProblem F) : ℕ

Coefficient degree cap used by the classical scalar-kernel PM-basis leaf.

def CompPoly.PolynomialMatrix.Approximant.coefficientEquationIndices (orders : Array ℕ) : Array (ℕ × ℕ)

Coefficient-equation indices (column, coefficientDegree).

def CompPoly.PolynomialMatrix.Approximant.coefficientMatrix {F : Type u_1} [Field F] (problem : XAdicProblem F) : DenseMatrix F

Dense scalar coefficient matrix for the bounded leaf problem.

def CompPoly.PolynomialMatrix.Approximant.coefficientMatrixRow {F : Type u_1} [Field F] (problem : XAdicProblem F) (degreeCap : ℕ) (equation : ℕ × ℕ) : Array F

One scalar coefficient row for the bounded leaf problem.

def CompPoly.PolynomialMatrix.Approximant.coefficientMatrixRows {F : Type u_1} [Field F] (problem : XAdicProblem F) : Array (Array F)

Scalar coefficient rows for the bounded leaf problem. This is the same matrix as coefficientMatrix, represented directly as row arrays for the tiny leaf RREF routine.

def CompPoly.PolynomialMatrix.Approximant.swapScalarRows {F : Type u_1} (rows : Array (Array F)) (rowA rowB : ℕ) : Array (Array F)

Swap two scalar rows in a row-array matrix.

def CompPoly.PolynomialMatrix.Approximant.findScalarPivotRow {F : Type u_1} [Field F] [BEq F] (rows : Array (Array F)) (startRow col : ℕ) : Option ℕ

Find a nonzero pivot row at or below startRow in column col.

def CompPoly.PolynomialMatrix.Approximant.normalizeScalarRow {F : Type u_1} [Field F] [BEq F] (row : Array F) (pivotCol : ℕ) : Array F

Scale a scalar row so that column pivotCol becomes one.

def CompPoly.PolynomialMatrix.Approximant.addScaledScalarRow {F : Type u_1} [Field F] (target source : Array F) (factor : F) : Array F

Add factor * source to target, using zero defaults for ragged rows.

def CompPoly.PolynomialMatrix.Approximant.normalizeAndEliminateScalarRows {F : Type u_1} [Field F] [BEq F] (rows : Array (Array F)) (pivotRow pivotCol : ℕ) : Array (Array F)

Normalize one pivot row and clear the pivot column in all other rows.

structure CompPoly.PolynomialMatrix.Approximant.ScalarRrefResult {F : Type u_1} : Type u_1

RREF result for a scalar row-array matrix.

• rows : Array (Array F)
• pivots : Array ℕ

def CompPoly.PolynomialMatrix.Approximant.scalarRrefRowsLoop {F : Type u_1} [Field F] [BEq F] (cols : ℕ) : ℕ → ℕ → ℕ → Array (Array F) → Array ℕ → ScalarRrefResult

Fuel-bounded row-array RREF for tiny scalar coefficient matrices.

def CompPoly.PolynomialMatrix.Approximant.scalarRrefRows {F : Type u_1} [Field F] [BEq F] (rows : Array (Array F)) (cols : ℕ) : ScalarRrefResult

Row-array RREF for tiny scalar coefficient matrices.

def CompPoly.PolynomialMatrix.Approximant.basisVectorForFreeColumnRows {F : Type u_1} [Field F] (rows : Array (Array F)) (pivots : Array ℕ) (cols free : ℕ) : Array F

Kernel basis vector for one free column of a row-array RREF matrix.

def CompPoly.PolynomialMatrix.Approximant.homogeneousKernelBasisRows {F : Type u_1} [Field F] [BEq F] (rows : Array (Array F)) (cols : ℕ) : Array (Array F)

Homogeneous scalar-kernel basis for a row-array matrix.

def CompPoly.PolynomialMatrix.Approximant.vectorToPolynomialRow {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (degreeCap solutionWidth : ℕ) (v : Array F) : PolynomialRow F

Convert one scalar kernel vector back into a polynomial row.

def CompPoly.PolynomialMatrix.Approximant.coeffXPower {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (c : F) (d : ℕ) : CPolynomial F

Polynomial c * X^d, built without the CPolynomial.monomial DecidableEq assumption.

def CompPoly.PolynomialMatrix.Approximant.polynomialScaleCoeffX {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (c : F) (d : ℕ) (p : CPolynomial F) : CPolynomial F

Multiply a row by c * X^d, using the coefficient-array monomial builder.

def CompPoly.PolynomialMatrix.Approximant.rowScaleCoeffX {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (c : F) (d : ℕ) (row : PolynomialRow F) : PolynomialRow F

Multiply a row by c * X^d, using coefficient shifting instead of generic polynomial multiplication by a monomial.

def CompPoly.PolynomialMatrix.Approximant.monomialUnitRow {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (width i d : ℕ) : PolynomialRow F

Monomial row X^d * e_i, used to complete bounded-kernel leaves to a full approximant basis.

def CompPoly.PolynomialMatrix.Approximant.kernelLeafCompletionRows {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (problem : XAdicProblem F) : PolynomialMatrix F

Trivial high-degree approximants present in every X-adic problem. These rows are essential when the bounded scalar kernel has fewer rows than the module rank.

def CompPoly.PolynomialMatrix.Approximant.rowsContainLeadingPosition {F : Type u_1} [Field F] [BEq F] (rows : PolynomialMatrix F) (shift : Array ℕ) (position : ℕ) : Bool

Whether a row set already contains a row with a given shifted leading position.

def CompPoly.PolynomialMatrix.Approximant.missingCompletionRows {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (problem : XAdicProblem F) (shift : Array ℕ) (rows : PolynomialMatrix F) : PolynomialMatrix F

High monomial rows for shifted leading positions not represented by rows. These rows are always valid approximants and keep recursive residual problems from losing coordinates after compact row reduction.

def CompPoly.PolynomialMatrix.Approximant.completeMissingPivotRows {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (problem : XAdicProblem F) (shift : Array ℕ) (rows : PolynomialMatrix F) : PolynomialMatrix F

Add high monomial approximants for missing pivot positions.

def CompPoly.PolynomialMatrix.Approximant.cancelKernelLeafLeadingTerm {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (target reducer : PolynomialRow F) (shift : Array ℕ) : PolynomialRow F

Cancel the shifted leading term of target by reducer, when their shifted leading positions agree. This is the small-leaf analogue of polynomial-matrix row reduction; it is used only after the bounded scalar kernel has already been computed.

def CompPoly.PolynomialMatrix.Approximant.kernelLeafConflictInRowStep? {F : Type u_1} [Field F] [BEq F] (rows : PolynomialMatrix F) (shift : Array ℕ) (i : ℕ) (found : Option (ℕ × ℕ)) (j : ℕ) : Option (ℕ × ℕ)

One inner-loop update for finding a leading-position conflict in a bounded kernel leaf.

def CompPoly.PolynomialMatrix.Approximant.kernelLeafConflictInRow? {F : Type u_1} [Field F] [BEq F] (rows : PolynomialMatrix F) (shift : Array ℕ) (i : ℕ) (found : Option (ℕ × ℕ)) : Option (ℕ × ℕ)

Scan one row for a shifted-leading-position conflict in a bounded kernel leaf.

def CompPoly.PolynomialMatrix.Approximant.kernelLeafConflictFrom? {F : Type u_1} [Field F] [BEq F] (rows : PolynomialMatrix F) (shift : Array ℕ) (found : Option (ℕ × ℕ)) : Option (ℕ × ℕ)

Scan all row pairs for the first shifted-leading-position conflict.

def CompPoly.PolynomialMatrix.Approximant.kernelLeafConflict? {F : Type u_1} [Field F] [BEq F] (rows : PolynomialMatrix F) (shift : Array ℕ) : Option (ℕ × ℕ)

First pair of nonzero bounded-kernel rows with the same shifted leading position.

def CompPoly.PolynomialMatrix.Approximant.reduceKernelLeafStep {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (rows : PolynomialMatrix F) (shift : Array ℕ) (i j : ℕ) : PolynomialMatrix F

One shifted-reduction step for bounded scalar-kernel rows.

def CompPoly.PolynomialMatrix.Approximant.reduceKernelLeafFuel {F : Type u_1} [Field F] [BEq F] (rows : PolynomialMatrix F) (shift : Array ℕ) : ℕ

Fuel for bounded-kernel shifted reduction. The scalar leaf is already a small base case, so this conservative degree-width bound is acceptable here.

def CompPoly.PolynomialMatrix.Approximant.pivotRows {F : Type u_1} [Field F] (pivots : Array (Option (PolynomialRow F))) : PolynomialMatrix F

Extract the nonempty pivot rows from a leading-position table.

def CompPoly.PolynomialMatrix.Approximant.insertKernelLeafPivotRowWithFuel {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] : ℕ → Array (Option (PolynomialRow F)) → Array ℕ → PolynomialRow F → Array (Option (PolynomialRow F))

Insert one row into a shifted weak-Popov pivot table. Conflicts are resolved only at the current leading position, avoiding the repeated global pair scans used by the simple reference reducer.

def CompPoly.PolynomialMatrix.Approximant.reduceKernelLeafRowsByPivots {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (rows : PolynomialMatrix F) (shift : Array ℕ) : PolynomialMatrix F

Pivot-table shifted reduction for bounded scalar-kernel rows.

def CompPoly.PolynomialMatrix.Approximant.reduceKernelLeafWithFuel {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] : ℕ → PolynomialMatrix F → Array ℕ → PolynomialMatrix F

Shift-reduce the bounded scalar-kernel rows before compacting them. This keeps one low representative per shifted leading position instead of selecting arbitrary low-degree kernel vectors.

def CompPoly.PolynomialMatrix.Approximant.reduceKernelLeafRows {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (rows : PolynomialMatrix F) (shift : Array ℕ) : PolynomialMatrix F

Shift-reduced bounded scalar-kernel rows for the PM-basis leaf.

def CompPoly.PolynomialMatrix.Approximant.insertKernelLeafRowIncremental {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (basis : PolynomialMatrix F) (shift : Array ℕ) (row : PolynomialRow F) : PolynomialMatrix F

Insert one bounded-kernel row into a small shifted-reduced leaf basis. This keeps the live reduction matrix near the module width instead of reducing the entire scalar kernel at once.

def CompPoly.PolynomialMatrix.Approximant.reduceKernelLeafRowsIncremental {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (rows : PolynomialMatrix F) (shift : Array ℕ) : PolynomialMatrix F

Shift-reduce all bounded scalar-kernel rows incrementally. The dense scalar kernel can have many rows, but after every insertion the weak-Popov conflict loop works on the current reduced basis plus one candidate row.

def CompPoly.PolynomialMatrix.Approximant.kernelLeafBasis {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (problem : XAdicProblem F) (shift : Array ℕ) : PolynomialMatrix F

Classical scalar-kernel leaf for small X-adic approximant problems.

def CompPoly.PolynomialMatrix.Approximant.compactNonzeroRows {F : Type u_1} [Field F] [BEq F] (rows : PolynomialMatrix F) : PolynomialMatrix F

Remove zero rows before a recursively computed approximant basis is used as the coordinate system for the next residual problem.