2 Theorems
\(q\) is reduced w.r.t. \(p\) if \(mainVar(q) {\lt} mainVar(p)\).
If \(mainVar(p) = mainVar(q)\), then \(q\) is reduced with respect to \(p\) if and only if \(q {\lt} p\).
\(mainVar(p) {\lt} mainVar(q)\) if \(p ≤ q\) and \(q\) is reduced with respect to \(p\).
\(init_i(p) = p\) if \(deg_i(p) = 0\) (i.e. \(x_i\) does not appear in \(p\)).
\(deg_i(init_i(p)) = 0\).
\(init_i(init_i(p)) = init_i(p)\).
\(\forall i j, deg_j(init_i(p)) \le deg_j(p)\)
\(init_i(p)\) is the leading coefficient when viewing \(p\) as a univariate polynomial in \(x_i\).
\(p = init_i(p) x_i ^d + q\), where \(deg_i(q) {\lt} d = deg_i(p)\).
\(deg_i(p + q) {\lt} deg_i(p)\) if \(deg_i(p) = deg_i(q)\) and \(init_i(p) + init_i(q) = 0\).
\(init_i(p \cdot q) = init_i(p) \cdot init_i(q)\) if there is no zero divisors in the coefficient ring.
\(mainVar(init(p)) {\lt} mainVar(p)\) for non-constant \(p\).
\(init_i(p)\) is reduced w.r.t. \(q\) if \(p\) is reduced w.r.t. to \(q\).
\(init_i(p)\) is reduced w.r.t. \(p\) for non-constant \(p\).
The set of Triangular Sets is well-founded under the lexicographic order ordering. This guarantees the termination of the Characteristic Set Algorithm.
If \(p \neq 0\) and is reduced with respect to \(S\), then modifying \(S\) by appending \(p\) (using "takeConcat") strictly decreases the order of \(S\).
\(deg_i(r) {\lt} deg_i(g)\) where \(r\) is the remainder of \(g\) by \(f\) w.r.t. \(i\) if \(deg_i(f) \ne 0\).
The remainder \(r\) of \(g\) by \(f\) is reduced with respect to \(f\) and satisfies \(init(f)^s \cdot g = q \cdot f + r\) for some \(s \in \mathbb {N}\) and \(q \in R[X_{\sigma }]\).
The remainder \(r\) of \(g\) by \(f\) satisfies \(deg_i(r) \le deg_i(g)\) if \(deg_i(f) = 0\)
The remainder \(r\) of \(g\) by a set \(S\) is reduced with respect to \(S\) and satisfies \((\prod S_i^{e_i}) \cdot g = \sum q_i \cdot S_i + r\) for some \(\{ e_i\} \) and \(\{ q_i\} \).
The remainder of \(g\) by \(f\) is \(0\) if \(f\) is a divisor of \(g\).
The remainder of \(g\) by \(f\) is \(g\) if \(deg_c(g) = 0\) where \(c = mainVar(f)\).
The remainder of \(p\) by a set \(S\) is \(0\) if \(p\) is in \(S\).
If \(p\) is in \(S\) and \(mainVar(p) \neq \bot \), then \(init(p)\) is in \(S\).
The algorithm computes a minimal standard ascending set contained in the input list.
The algorithm computes a minimal weak ascending set contained in the input list.
Appending an element which is reduced w.r.t. the basic set of list strictly decreases the order. Crucial for proving termination of characteristic set and zero decomposition algorithms.
Well-ordering principle (1): \(Zero(CS/IP) \subseteq Zero(PS)\), where \(IP\) is the initial-product of \(CS\).
Well-ordering principle (2): \(Zero(CS/IP) = Zero(PS/IP)\), where \(IP\) is the initial-product of \(CS\).
Well-ordering principle (3):
.
The algorithm computes a valid characteristic set for the input list.
The computed characteristic set is an ascending set.
The order of computed characteristic set \(\le \) the order of the input list.
\(\forall CS \in \mathcal{ZD}(PS), g \in PS\), \(0\) is the remainder of \(g\) by \(CS\).
Zero Decomposition Theorem: The zero set of a polynomial system \(PS\) is the union of the zero sets of the triangular systems computed by the algorithm:
.