Recursive PM-Basis Driver

Runtime data for recursive PM-basis computation, the fuel-bounded divide-and-conquer driver, root normalization, the pmBasis entry point, and the PMBasisContext contract structure.

References

• [Beckermann, B., and Labahn, G., A uniform approach for the fast computation of matrix-type Pade approximants][BL94]
• [Giorgi, P., Jeannerod, C.-P., and Villard, G., On the complexity of polynomial matrix computations][GJV03]

structure CompPoly.PolynomialMatrix.Approximant.PMBasisRuntime (F : Type u_2) [Field F] [BEq F] [LawfulBEq F] : Type u_2

Runtime data for recursive PM-basis computation.

• mulContext : CPolynomial.MulContext F
• lowMulContext : MulLowContext F
• composeBasis : PolynomialMatrix F → PolynomialMatrix F → PolynomialMatrix F
• residualProduct : Array ℕ → PolynomialMatrix F → PolynomialMatrix F → PolynomialMatrix F
• leafCutoff : ℕ
• leafBasis : XAdicProblem F → Array ℕ → PolynomialMatrix F

def CompPoly.PolynomialMatrix.Approximant.kernelLeafRuntimeWithLowAndCompose {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (mulCtx : CPolynomial.MulContext F) (lowCtx : MulLowContext F) (leafCutoff composeLeafCutoff : ℕ) : PMBasisRuntime F

Recursive PM-basis runtime using the scalar dense-kernel routine as its small-leaf solver and an independently tuned basis-composition cutoff.

def CompPoly.PolynomialMatrix.Approximant.kernelLeafRuntimeWithLow {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (mulCtx : CPolynomial.MulContext F) (lowCtx : MulLowContext F) (leafCutoff : ℕ) : PMBasisRuntime F

Recursive PM-basis runtime using the scalar dense-kernel routine as its small-leaf solver.

def CompPoly.PolynomialMatrix.Approximant.kernelLeafRuntime {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (mulCtx : CPolynomial.MulContext F) (leafCutoff : ℕ) : PMBasisRuntime F

Compatibility runtime whose low products are obtained by truncating full products.

def CompPoly.PolynomialMatrix.Approximant.pmBasisWithFuelCore {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (runtime : PMBasisRuntime F) : ℕ → XAdicProblem F → Array ℕ → PolynomialMatrix F

Fuel-bounded recursive PM-basis driver, compacting zero rows after each leaf and composition step.

Internal nodes return the composed product P₂ * P₁ without re-reduction: composition of minimal half-bases under the updated shift is itself a basis of the full-order approximant module, so re-reducing at every node would only add work that is quadratic in the row degrees and outside the PM-basis cost model. A single weak-Popov normalization pass runs once at the root entry points.

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

Root normalization for a recursively composed approximant basis: one weak-Popov reduction pass plus completion rows for any leading position that lost its representative. When the recursion preserved minimality this pass performs no cascading cancellations; it is a semantic guard, not part of the recursive cost model.

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

Fuel-bounded recursive PM-basis driver with root normalization.

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

Default fuel choice, large enough to split each positive order down to the leaf cutoff.

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

Recursive PM-basis entry point.

theorem CompPoly.PolynomialMatrix.Approximant.completeMissingPivotRows_size_pos {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (problem : XAdicProblem F) (shift : Array ℕ) (rows : PolynomialMatrix F) (hsize : 0 < Array.size problem.matrix) : 0 < Array.size (completeMissingPivotRows problem shift rows)

Monomial completion never returns an empty matrix for problems with at least one module row: an empty candidate set is completed with one monomial row per module coordinate.

theorem CompPoly.PolynomialMatrix.Approximant.pmBasisNormalizeRoot_size_pos {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (problem : XAdicProblem F) (shift : Array ℕ) (basis : PolynomialMatrix F) (hsize : 0 < Array.size problem.matrix) : 0 < Array.size (pmBasisNormalizeRoot problem shift basis)

The root-normalized recursive PM-basis is nonempty for problems with at least one module row.

structure CompPoly.PolynomialMatrix.Approximant.PMBasisContext (F : Type u_2) [Field F] [BEq F] [LawfulBEq F] : Type u_2

Context packaging the executable PM-basis operation with theorem fields.

• runtime : PMBasisRuntime F
• basis : XAdicProblem F → Array ℕ → PolynomialMatrix F
• sound (problem : XAdicProblem F) (shift : Array ℕ) (row : PolynomialRow F) : row ∈ (self.basis problem shift).MatrixRows → ∀ j < problem.orders.size, truncateX (problem.orders.getD j 0) (rowGet (rowMulMatrixWith self.runtime.mulContext row problem.matrix) j) = 0
• complete_minimal (problem : XAdicProblem F) (shift : Array ℕ) (row : PolynomialRow F) : 0 < Array.size problem.matrix → problem.matrix.WellFormed → (∀ j < problem.orders.size, truncateX (problem.orders.getD j 0) (rowGet (rowMulMatrixWith self.runtime.mulContext row problem.matrix) j) = 0) → rowIsZero row = false → Array.size row ≤ Array.size problem.matrix → ∃ (basisRow : PolynomialRow F) (degree : ℕ), basisRow ∈ (self.basis problem shift).MatrixRows ∧ Array.size basisRow ≤ Array.size problem.matrix ∧ rowShiftedDegree? basisRow shift = some degree ∧ ∀ (rowDegree : ℕ), rowShiftedDegree? row shift = some rowDegree → degree ≤ rowDegree