1 Introduction

Many systems of differential equations do not admit closed-form solutions in “elementary” functions and hence cannot be solved symbolically. Despite this, increasingly good heuristics are implemented in computer algebra systems to find solutions [3, 4]. Given such a set of closed-form solutions returned by a computer algebra system, the question remains whether this set is the complete solution set. More generally, the goal of this paper is to “measure” the sizes of solution sets \(U\subseteq V\) in order to decide whether \(U=V.\)

There are many classical measures of the size of the solution set (cf. [19] for an overview), the strongestFootnote 1 of which is Kolchin’s dimension polynomial [10, 13]. However, the dimension polynomial can only describe solution sets given by characterizable differential ideals and only the dimension of such solution sets, but no finer details (cf. Example 4.9). It was a great surprise to the author that such finer details can appear in the solution set of a differential equation, for example countable infinite exceptional sets (cf. Example 4.8).

This paper introduces the differential counting polynomial, a more detailed description of a solution set of a system of differential equations. If it exists, it generalizes the dimension polynomial (Theorem 4.5) and decides in many cases whether solution sets are equal (Theorem 4.3 and Proposition 4.4).

The idea of the differential counting polynomial originates from Plesken’s algebraic counting polynomial [16]. The algebraic counting polynomial is an element \(c(V)\in {\mathbb {Z}}[\infty ]\) which describes the size of a constructible set V in affine n-space. Here, \(\infty \) is a free indeterminate, which can be thought of as representing the cardinality of an affine 1-space. For example, the algebraic counting polynomial of an affine i-space is \(\infty ^i\in {\mathbb {Z}}[\infty ]\), and if V is a j-fold unramified cover of W, then \(c(V)=j\cdot c(W)\in {\mathbb {Z}}[\infty ]\). Two constructible sets \(U\subseteq V\) are equal if and only if their algebraic counting polynomials c(U) and c(V) coincide.

The differential counting polynomial is the algebraic counting polynomial for the different Taylor polynomials of degree \(\ell \) of all formal power series solutions. We restrict to formal power series solutions as they exist in a formally consistent system of differential equations for any formal power series given as initial data. Similar results hold for analytic [18] but not for smooth initial data (cf. Lewy’s example [15]).

Determining the differential counting polynomial of a set of differential equations is not algorithmic in general. Even in the case of a single inhomogeneous linear differential equation, the problem of the existence of formal power series solutions can be reduced to Hilbert’s unsolvable tenth problem about Diophantine equations [5]. Also, the existence of the differential counting polynomial is still an open problem. However, the author succeeded in computing the differential counting polynomial using Theorem 4.6 and inductive proofs similar to Examples 4.8 and 4.9 for all of the various classes of examples of differential equations he encountered.

So, it is hard to determine the differential counting polynomial from a set of differential equations without explicitly knowing the corresponding full set of solutions V. In contrast, the differential counting polynomial c(U) of an explicitly given set of solutions U can be computed more easily by determining how unrestrictedly the power series coefficients of elements in U are choosable (cf. Example 4.9). Once the differential counting polynomial c(V) of V is known, one can often decide whether an explicitly given set of solutions U is equal to the complete set of solutions V by comparing c(U) and c(V).

Sections 2 and 3 recapitulate simple systems and Plesken’s algebraic counting polynomial, respectively, and generalize them for our needs. In Sect. 4, we define the differential counting polynomial, state its basic properties, and give examples. The author’s PhD thesis [14] contains additional (classes of) examples. The proofs follow in Sect. 5.

2 Simple \(\sigma \)-Systems

Simple systems stratify constructible sets into sets with convenient geometric properties. Such systems underlie Plesken’s counting polynomial. This section recapitulates simple systems and generalizes them to describe differential equations.

Let \(R:={\mathbb {C}}[y_1,\ldots ,y_n]\) be a polynomial ring. We fix the total order, called ranking, \(y_1<y_2<\cdots <y_n\) on \(\{y_1,\ldots ,y_n\}\). The <-greatest variable \({{\mathrm{ld}}}(p)\) occurring in \(p\in R\setminus {\mathbb {C}}\) is called leader of p. The coefficient \({{\mathrm{ini}}}(p)\) of the highest power of \({{\mathrm{ld}}}(p)\) in p is called the initial of p. For \(S\subset R\setminus {\mathbb {C}}\) define \({{\mathrm{ld}}}(S):=\{{{\mathrm{ld}}}(p)|p\in S\}\) and similarly \({{\mathrm{ini}}}(S)\). Denote by \(S_{<y_i}\), \(S_{\le y_i}\), and \(S_{y_i}\) the sets \(S\cap {\mathbb {C}}[y_1,\ldots ,y_{i-1}]\), \(S\cap {\mathbb {C}}[y_1,\ldots ,y_i]\), and \(\{p\in S\mid {{\mathrm{ld}}}(p)=y_i\}\), respectively, for all \(1\le i\le n\).

We call a set of finitely many equations and countably many inequations a \(\sigma \)-system. If this set is finite, we call it system. Let S be a \(\sigma \)-system over R. We denote the set of solutions in \({\mathbb {C}}^n\) of S by \({\mathfrak {Sol}}(S)\). Call S weakly triangular if it contains no equation or inequation in \({\mathbb {C}}\) and it contains either at most one equation or arbitrary many inequations of leader \(y_i\) for each \(1\le i\le n\). We say that S has non-vanishing initials if no initial vanishes when substituting an \(\mathbf {a}\in {\mathfrak {Sol}}(S)\). Substituting all indeterminates \(y_i\not ={{\mathrm{ld}}}(p)\) in \(p\in S\) by an \(a_i\in {\mathbb {C}}\) results in a univariate polynomial. If all these univariate polynomials resulting from the \(p\in S\) and \(\mathbf {a}\in {\mathfrak {Sol}}(S)\) are square-free, then we call S square-free. We call S a simple \(\sigma \) -system if it is weakly triangular, has non-vanishing initials, and is square-free.

A set \(\{S_1\ldots ,S_l\}\) of simple \(\sigma \)-systems with disjoint solution sets is called an algebraic Thomas decomposition of a \(\sigma \)-system S if \({\mathfrak {Sol}}(S)=\biguplus _{1\le i\le l}{\mathfrak {Sol}}(S_i)\). Such a Thomas decomposition is called comprehensive with respect to an indeterminate \(y_k\) if \({\mathfrak {Sol}}((S_i)_{\le y_k})\cap {\mathfrak {Sol}}((S_j)_{\le y_k})\in \{\emptyset ,{\mathfrak {Sol}}(S_i)\}\) for all \(1\le i,j\le l\).

3 Algebraic Counting Polynomials

This section recapitulates Plesken’s algebraic counting polynomial for constructible sets [16, 17] and generalizes it to be suitable for describing differential equations. We consider the affine n-space \({\mathbb {C}}^n\) with projections \(\pi _i:{\mathbb {C}}^n\rightarrow {\mathbb {C}}^i:(a_1,\ldots ,a_n)\mapsto (a_1,\ldots ,a_i)\).

Definition 3.1

The following four axioms iterativelyFootnote 2 applied to a constructible set \(V\subseteq {\mathbb {C}}^n\) yield its algebraic counting polynomial, an element in the univariate polynomial ring \({\mathbb {Z}}[\infty ]\).

  1. (1)

    \(c(V)=|V|\) if V is finite.

  2. (2)

    \(c(V)=\infty \) for an affine 1-space V over \({\mathbb {C}}\).

  3. (3)

    \(c(V\uplus W)=c(V)+c(W)\) for disjoint constructible sets \(V,W\subset {\mathbb {C}}^n\).

  4. (4)

    If \(V\subset {\mathbb {C}}^n\) is constructible and for some \(1\le i\le n\) each non-empty fiber W of \(\pi _i\) has the same value under c, then \(c(V)=c(W)\cdot c(\pi _i(V))\).

The algebraic Thomas decomposition makes the computation of the algebraic counting polynomial algorithmic [16]. The following theorem shows how the algebraic counting polynomial can be used to compare constructible sets. Our goal is a similar theorem for solution sets of differential equations.

Theorem 3.2

[16, Cor. 3.4] Let \(U\subseteq V\subseteq {\mathbb {C}}^n\) be constructible sets. Then \(U=V\) if and only if \(c(U)=c(V)\).

In solution sets of differential equations, countable exceptional sets appear naturally (cf. Example 4.8). To describe these sets, we generalize the algebraic counting polynomial.

Definition 3.3

Let \(V\subseteq {\mathbb {C}}^n\). Then, call any element c(V) in the polynomial ring \({\mathbb {Z}}[\infty ,\aleph _0]\) constructed by iteratively applying the four axioms from Definition 3.1 above and the following fifth axiom an algebraic counting polynomial of V.

  1. (5)

    \(c({\mathbb {C}}^1\setminus M)=\infty -\aleph _0\) for \(M\subset {\mathbb {C}}^1\) is countably infinite.

Remark 3.4

In general, the algebraic counting polynomial is not unique. For example, the set \({\mathfrak {Sol}}(\{x-i\not =0|i\in {\mathbb {Z}}_{\ge 0}\})={\mathfrak {Sol}}(\{x-i\not =0|i\in {\mathbb {Z}}_{\ge 1}\})\uplus \{0\}\) can have both algebraic counting polynomial \(\infty -\aleph _0\) and \(\infty -\aleph _0+1\). Hence, Theorem 3.2, which states that the algebraic counting polynomial decides equality of contained constructible sets, cannot hold in general, but it holds for the important special case of well-fibered sets (cf. Theorem 3.6).

Even worse, it is not clear in which cases an algebraic counting polynomial exists, i.e., that there exists a way to apply the axioms terminating in an element in \({\mathbb {Z}}[\infty ,\aleph _0]\). Simple algebraic \(\sigma \)-systems are a first example where existence (and some uniqueness) holds.

Theorem 3.5

Let \(S\subset {\mathbb {C}}[y_1,\ldots ,y_n]\) be a simple algebraic \(\sigma \)-system. Then an algebraic counting polynomial of \({\mathfrak {Sol}}(S)\) exists.

Consider counting polynomials as polynomials in the indeterminate \(\infty \). Then degree and leading coefficient of any algebraic counting polynomial \(c({\mathfrak {Sol}}(S))\) are equal to those of the (unique, cf. [16, Prop. 3.3]) counting polynomial \(c(\overline{{\mathfrak {Sol}}(S)})\) of its Zariski closure \(\overline{{\mathfrak {Sol}}(S)}\). In particular, the degree of \(c({\mathfrak {Sol}}(S))\) is equal to the dimension of \(\overline{{\mathfrak {Sol}}(S)}\).

In particular, the degrees and leading coefficients of these algebraic counting polynomials are well defined and the leading coefficients are natural numbers. We postpone the proof of this theorem to p. 14.

Countable exceptional sets complicate the use of the algebraic counting polynomial for \(\sigma \)-systems in applications. However, the counting polynomial is well behaved for well-fibered sets, which we define as sets with a counting polynomial in \({\mathbb {Z}}[\infty ]\). These sets behave similarly as constructible sets with regard to algebraic counting polynomials; in particular the algebraic counting polynomial is strong enough to decide equality of such sets contained in each other.

Theorem 3.6

Let \(U\subseteq V\subseteq {\mathbb {C}}^n\) be two well-fibered sets. Then \(U=V\) if and only if \(c(U)=c(V)\). In particular, the counting polynomial of well-fibered sets is well defined in the sense that it is unique.

We postpone the proof of this theorem to p. 15.

Even when \(\aleph _0\) appears in algebraic counting polynomials of two sets \(U\subseteq V\), one might be able to prove \(U\not =V\) by estimating the algebraic counting polynomial. First, any subset of \({\mathbb {C}}^1\) with a countably infinite complement can be enlarged to a set with finite complement. Second, any subset of \({\mathbb {C}}^1\) with a countably infinite complement can be shrunk to a finite set. Thus, for \(p(\aleph _0,\infty )\in {\mathbb {Z}}[\aleph _0,\infty ]\) and \(q(\infty )\in {\mathbb {Z}}[\infty ]\) we define \(p\prec q\) if \(p(\infty -k,\infty )=q(\infty )\) and \(p\succ q\) if \(p(k,\infty )=q(\infty )\) for some \(k\in {\mathbb {Z}}_{\ge 0}\). Additionally, we use the total order \(q<q'\) if there exists an \(x_0\) with \(q(x)<q'(x)\) for all \(x>x_0\) for \(q,q'\in {\mathbb {Q}}[\infty ]\).

Proposition 3.7

Let \(U\subseteq V\subseteq {\mathbb {C}}^n\) have algebraic counting polynomials \(p_1(\aleph _0,\infty ):=c(U)\) and \(p_2(\aleph _0,\infty ):=c(V)\). If there exist \(q_1,q_2\in {\mathbb {Z}}[\infty ]\) with \(p_1\prec q_1\lneqq q_2\prec p_2\), then \(U\not =V\).

The proof of this proposition is a natural generalization of one implication of the proof of [16, Cor. 3.4].

4 The Differential Counting Polynomial

This section defines the differential counting polynomial and states some of its properties. Beforehand, we fix some notation.

4.1 Preliminaries

Let \(F\supseteq {\mathbb {C}}\) be a field of meromorphic functions in n complex variables \(x_1,\ldots ,x_n\), and \(\Delta =\{\partial _{x_1},\ldots ,\partial _{x_n}\}\) the corresponding set of partial differential operators. Let \(U:=\{ u^{(1)}, \ldots , u^{(m)} \}\) be a set of differential indeterminates and define \(u^{(j)}_\mu :=\partial ^\mu u^{(j)}\) for \(\partial ^\mu := \partial ^{\mu _1}_{x_1}\ldots \partial ^{\mu _n}_{x_n}\), \(\mu \in ({\mathbb {Z}}_{\ge 0})^n\). The differential polynomial ring \(F\{U\}\) is the infinitely generated polynomial ring in the indeterminates \(\{U\}_\Delta :=\{u^{(j)}_\mu | 1\le j\le m, \mu \in ({\mathbb {Z}}_{\ge 0})^n\}\). Denote by \(F\{U\}_{\le \ell }\) its subring of elements of order at most \(\ell \) The derivations \(\partial _{x_i}: F \rightarrow F\) extend to \(\partial _{x_i}: F\{U\} \rightarrow F\{U\}\) via additivity and Leibniz rule. Let \({\text {sep}}(p)\) be the separant of \(p\in F\{U\}\). A ranking of \(F\{U\}\) is a total ordering < of \(\{U\}_\Delta \) satisfying the two properties (1) \(u^{(j)}_\mu <\partial u^{(j)}_\mu \) and (2) \(u^{(j)}_\mu <u^{(j')}_{\mu '}\) implies \(\partial u^{(j)}_\mu <\partial u^{(j')}_{\mu '}\) for all \(u^{(j)}_\mu , u^{(j')}_{\mu '}\in \{U\}_\Delta \) and \(\partial \in \Delta \). A ranking < is called orderly if \(|\mu |<|\mu '|\) implies \(u^{(j)}_{\mu } < u^{(j')}_{\mu '}\), where \(|\mu |:=\mu _1+\cdots +\mu _n\). In what follows, we fix an orderly ranking < on \(F\{U\}\).

Now, we extend the formalism of differential algebra to incorporate algebraic constraints for power series coefficients. We consider the set

$$\begin{aligned} G:=G(U,\Delta ):=\left\{ g_{\mu }^{(j)}\mid \mu \in {\mathbb {Z}}_{\ge 0}^n,1\le j\le m\right\} \end{aligned}$$

of indeterminates and call the polynomial ring \({\mathbb {C}}[G]\) the polynomial ring of power series coefficients. The bijection \(\rho :\{U\}_\Delta \rightarrow G(U,\Delta ):u^{(j)}_{\mu }\mapsto g^{(j)}_{\mu }\) extends the orderly ranking < on \(F\{U\}\) to an (algebraic) ranking on \({\mathbb {C}}[G]\). For \(\ell \in {\mathbb {Z}}_{\ge 0}\) let \({\mathbb {C}}[G]_{\le \ell }\) be the subring generated by all indeterminates \(g_{\mu }^{(j)}\) of order \(|\mu |\le \ell \).

We call a union of finitely many differential equations in \(F\{U\}\), finitely many power series coefficient equations in \({\mathbb {C}}[G]\), and countably many power series coefficient inequations in \({\mathbb {C}}[G]\) an algebraically restricted \(\sigma \) -system of differential equations and an algebraically restricted system of differential equations if it is finite.

We are concerned with power series solutions in the power series ring \(P_\zeta :={\mathbb {C}}[[x_1-\zeta _1,\ldots ,x_n-\zeta _n]]\) centered around \(\zeta =(\zeta _1,\ldots ,\zeta _n)\in {\mathbb {C}}^n\). We interpret equations in \(F\{U\}\) as equations for functions, e.g., \(u^{(1)}_{(0,\ldots ,0)}=0\) implies that \(u^{(1)}\) is the zero function, whereas equations in \({\mathbb {C}}[G]\) are equations for single power series coefficients, e.g., \(g^{(1)}_{(0,\ldots ,0)}=0\) implies that \(u^{(1)}\) has a zero at its center of expansion \(\zeta \). More precisely, a solution of power series coefficient equations or inequations is defined as a tuple of power series \(f\in P_\zeta ^U\cong \bigoplus _UP_\zeta \) that evaluates to zero or non-zero, respectively, when substituting \(g_{\mu }^{(j)}\) by the coefficient of \((x_1-\zeta _1)^{\mu _1}\ldots (x_n-\zeta _n)^{\mu _n}\) in \(f(u^{(j)})\). Our definition of a solution of a differential equation in \(F\{U\}\), where all coefficients are holomorphic in \(\zeta \), is the usual one. Denote the set of formal power series solutions of an algebraically restricted \(\sigma \)-system of differential equations S around \(\zeta \) by \({\mathfrak {Sol}}_\zeta (S)\subseteq P_\zeta ^U\).

We consider Taylor polynomials which extend to a Taylor series. Let \(P_{\zeta ,>\ell }^U\) be the \(P_\zeta \)-submodule of \(P_\zeta ^U\) generated by the \(u^{(j)}\mapsto (x_1-\zeta _1)^{\mu _1}\ldots (x_n-\zeta _n)^{\mu _n}\) for \(\mu \in {\mathbb {Z}}_{\ge 0}^n\) with \(|\mu |>\ell \). Define the set \({\mathfrak {Sol}}_\zeta (S)_{\le \ell }\) of formal power series solutions of S around \(\zeta \) truncated at order \(\ell \) as the image of \({\mathfrak {Sol}}_\zeta (S)\) in \(P_\zeta ^U/P_{\zeta ,>\ell }^U\) under the natural epimorphism \(P_\zeta ^U\twoheadrightarrow P_\zeta ^U/P_{\zeta ,>\ell }^U\).

4.2 Definition of the Differential Counting Polynomial

The algebraic Thomas decomposition computes the algebraic counting polynomial. For differential equations, there is a similar decomposition.

Theorem 4.1

Let S be an algebraically restricted system of differential equations, such that the center of expansion \(\zeta \in {\mathbb {C}}^n\) is not a pole of any coefficient of a differential equation. Let \(\ell \in {\mathbb {Z}}_{\ge 0}\). There exists a countable set C of simple algebraic \(\sigma \)-systems in \({\mathbb {C}}[G]_{\le \ell }\) with

$$\begin{aligned} {\mathfrak {Sol}}_\zeta (S)_{\le \ell }=\biguplus _{\widetilde{S}\in C}{\mathfrak {Sol}}_\zeta (\widetilde{S})_{\le \ell }. \end{aligned}$$

We postpone the proof of this theorem to p. 16. This theorem justifies the following definition of the differential counting polynomial.

Definition 4.2

Let S be an algebraically restricted system of differential equations. Let \(C_\ell \) be a countable set of algebraic \(\sigma \)-systems with \({\mathfrak {Sol}}_\zeta (S)_{\le \ell }=\biguplus _{\widetilde{S}\in C_\ell }{\mathfrak {Sol}}_\zeta (\widetilde{S})_{\le \ell }\) for each \(\ell \in {\mathbb {Z}}_{\ge 0}\).

If an algebraic counting polynomial exists for \(C_\ell \), then define an \(\ell \)-th differential counting polynomial of S as \(c(C_\ell )\in {\mathbb {Z}}[\infty ,\aleph _0]\). If an \(\ell \)th differential counting polynomial exists for all \(\ell \), then define a counting sequence \(c(S)\in {\mathbb {Z}}[\infty ,\aleph _0]^{{\mathbb {Z}}_{\ge 0}}\) of S (or \({\mathfrak {Sol}}_\zeta (S)\)) as

$$\begin{aligned} c(S): \ell \mapsto c(C_\ell ). \end{aligned}$$

If there exists a \(p\in {\mathbb {Q}}[\ell ,\aleph _0,\infty ,\infty ^\ell ,\infty ^{\frac{\ell ^2}{2!}},\ldots ,\infty ^{\frac{\ell ^n}{n!}}]\) such that \(c(S)(\ell )=p\) for ultimately all \(\ell \), then call p a differential counting polynomial of S (or \({\mathfrak {Sol}}_\zeta (S)\)) and denote it by \(\bar{c}(S)\). For a differential ideal \(I=\langle p_1,\ldots ,p_k\rangle _\Delta \) define \(c(I):=c(\{p_1,\ldots ,p_k\})\) and \(\bar{c}(I):=\bar{c}(\{p_1,\ldots ,p_k\})\).

We write \(\infty ^{\ell ^2}\) instead of \((\infty ^{\frac{\ell ^2}{2!}})^2\) and use similar simplifications.

The existence of a differential counting sequence or a differential counting polynomial is not clear, in general.

4.3 Deciding Equality of Sets

The following theorem and proposition use counting sequences and differential counting polynomials to decide equality of sets contained in each other.

Theorem 4.3

Let \(S_1,S_2\) be two algebraically restricted systems of differential equations with \({\mathfrak {Sol}}_\zeta (S_1)\subseteq {\mathfrak {Sol}}_\zeta (S_2)\).

  1. 1

    Assume that both counting sequences \(c(S_1)\) and \(c(S_2)\) exist and that \(c(S_1)(\ell ), c(S_2)(\ell )\in {\mathbb {Z}}[\infty ]\) for all \(\ell \in {\mathbb {Z}}_{\ge 0}\). Then \({\mathfrak {Sol}}_\zeta (S_1)={\mathfrak {Sol}}_\zeta (S_2)\) if and only if \(c(S_1)(\ell )=c(S_2)(\ell )\) for all \(\ell \in {\mathbb {Z}}_{\ge 0}\). In particular, \(c(S_1)\) is the unique counting sequence of \(S_1\).

  2. 2

    Assume both differential counting polynomials \(\bar{c}(S_1)\) and \(\bar{c}(S_2)\) exist and \(\bar{c}(S_1),\bar{c}(S_2)\in {\mathbb {Q}}[\ell ,\infty ,\infty ^\ell ,\infty ^{\frac{\ell ^2}{2!}},\ldots ,\infty ^{\frac{\ell ^n}{n!}}]\) holds. Then \({\mathfrak {Sol}}_\zeta (S_1)={\mathfrak {Sol}}_\zeta (S_2)\) if and only if \(\bar{c}(S_1)=\bar{c}(S_2)\). In particular, \(\bar{c}(S_1)\) is the unique differential counting polynomial of \(S_1\).

The sets \({\mathfrak {Sol}}_\zeta (S_1)_{\le \ell }\) and \({\mathfrak {Sol}}_\zeta (S_2)_{\le \ell }\) of formal power series solutions truncated at order \(\ell \) are well-fibered under the conditions of (4.3) and well-fibered for high enough \(\ell \) under the conditions of (4.3). Thus, this theorem is a corollary of Theorem 3.6.

Remark 3.4 indicates that a stronger version of this theorem is unlikely. However, we can show that two sets are not equal in the differential case similar to Proposition 3.7, by using the total order < and the estimation \(\prec \), both defined before Proposition 3.7.

Proposition 4.4

Let \(S_1,S_2\) be two algebraically restricted systems of differential equations with \({\mathfrak {Sol}}_\zeta (S_1)\subseteq {\mathfrak {Sol}}_\zeta (S_2)\) such that the counting sequences \(c(S_1)\) and \(c(S_2)\) exist. If there exist an \(\ell \in {\mathbb {Z}}_{\ge 0}\) and \(q_1,q_2\in {\mathbb {Z}}[\infty ]\) with \(c(S_1)(\ell )\prec q_1\lneqq q_2\prec c(S_2)(\ell )\), then \({\mathfrak {Sol}}_\zeta (S_1)\not ={\mathfrak {Sol}}_\zeta (S_2)\).

This proposition follows from Proposition 3.7 just as Theorem 4.3 follows from Theorem 3.6.

4.4 Comparison to the Differential Dimension Polynomial

The counting sequence and the differential counting polynomial are connected to the differential dimension polynomial (cf. [9, 10, 12, 13]) in the version defined for characterizable differential ideals (cf. [6, 7]).

For the following theorem, we consider an \(\ell \)th differential counting polynomial as a polynomial in the indeterminate \(\infty \) and coefficients in \({\mathbb {Z}}[\aleph _0]\). Similarly, we consider a differential counting polynomial as a polynomial in the indeterminates \(\infty ^{\frac{\ell ^i}{i!}}\) for \(0\le i\le n\) and coefficients in \({\mathbb {Q}}[\aleph _0,\ell ]\). We order the indeterminates \(\infty ^{\frac{\ell ^n}{n!}}>\cdots>\infty ^{\frac{\ell ^2}{2!}}>\infty ^\ell >\infty \).

Theorem 4.5

Let \(I:=\langle S\rangle _\Delta :({{\mathrm{ini}}}(S)\cup {\text {sep}}(S))^\infty \) be a characterizable differential ideal given by a regular chain S. Denote by

$$\begin{aligned} \Omega _I:{\mathbb {Z}}_{\ge 0}\mapsto {\mathbb {Z}}_{\ge 0}:\ell \mapsto \dim (F\{U\}_{\le \ell }/(I\cap F\{U\}_{\le \ell })) \end{aligned}$$

its differential dimension function and by \(\omega _I(l)\) its dimension polynomial, the unique polynomial that agrees with the dimension function for all large enough \(\ell \). If an \(\ell \)th differential counting polynomial \(c(I)(\ell )\) of I exists, then its leading term is

$$\begin{aligned} \left( \mathop {\prod _{p\in S}}\limits _{{{\mathrm{ord}}}(p)\le \ell }\deg _{{{\mathrm{ld}}}(p)}p\right) \cdot \infty ^{\Omega _I(\ell )}. \end{aligned}$$

If a differential counting polynomial \(\bar{c}(I)\) of I exits, then its leading term is

$$\begin{aligned} \left( \prod _{p\in S}\deg _{{{\mathrm{ld}}}(p)}p\right) \cdot \infty ^{\omega _I(\ell )}. \end{aligned}$$

We postpone the proof to p. 17.

Under the assumptions of this theorem, the differential counting polynomial implies the same invariants of differential birational maps as the differential dimension polynomial. In particular, the differential type, typical dimension, and differential dimension can be read off the exponent of \(\infty \) in the leading term. This exponent is a polynomial in \(\ell \) equal to the differential dimension polynomial. The differential type t is the degree of this exponent, and when writing it as \(\sum _{i=0}^na_i\left( {\begin{array}{c}\ell +i\\ i\end{array}}\right) \) the typical dimension is \(a_t\) and the differential dimension is \(a_n\) (cf. [13, Theorem 1.1]).

4.5 Simple Differential Systems without Inequations

For semilinear systems of differential equations there exists a closed formula for the differential counting polynomial that holds once all differential consequences are obvious from the system (such systems are called passive [8], involutive [2] or coherent [11]). It follows from this formula that the differential counting polynomial of such systems does not involve \(\aleph _0\). This holds for the more general class of differential equations given by a simple differential system S without inequations [2, Def. 3.5]. Let \({\mathcal {I}}(S):=\langle T\rangle _\Delta :q^\infty \) be the corresponding characterizable differential ideal, where T are the equations in S and q is the product of the initials and separants of T. Let \(\Omega _{{\mathcal {I}}(S)}\) denote its differential dimension function and \(\omega _{{\mathcal {I}}(S)}\) its dimension polynomial [13].

Theorem 4.6

Let \(S=\{p_1,\ldots ,p_s\}\) be a simple differential system in \(F\{U\}\) without inequations. Consider formal power series solutions around a point \(\zeta \in {\mathbb {C}}^n\) such that neither evaluating the coefficients of S at \(\zeta \) yields a pole nor any initial or separant vanishes identically. Then, its unique counting sequence is

$$\begin{aligned} c(S):l\mapsto \left( \prod _{{\begin{array}{c} 1\le i\le s\\ {{\mathrm{ord}}}(p_i)\le \ell \end{array}}}\deg _{{{\mathrm{ld}}}(p_i)}(p_i)\right) \cdot \infty ^{\Omega _{{\mathcal {I}}(S)}(\ell )}, \end{aligned}$$

and its differential counting polynomial is

$$\begin{aligned} \bar{c}(S)=\left( \prod _{{1\le i\le s}}\deg _{{{\mathrm{ld}}}(p_i)}(p_i)\right) \cdot \infty ^{\omega _{{\mathcal {I}}(S)}(\ell )}. \end{aligned}$$

We postpone the proof to p. 17.

Differential inequations in the sense of Thomas (cf. [2]) are not well-suited to count power series solutions, as \(u(x)\not =0\) just implies that at least one power series coefficient of u is non-zero.

Many examples of systems of differential equations yield a Thomas decomposition into a single simple differential system without inequations. Examples are systems of linear differential equations and semilinear formally integrable systems of differential equations. We show an example of the latter class.

Example 4.7

Let \(F={\mathbb {C}}\), \(\Delta =\{\partial _x,\partial _y, \partial _z, \partial _t \}\), \(U=\{u,v,w,p\}\), and fix a ranking, such that the leaders are the underlined indeterminates. The incompressible Navier–Stokes equations are

$$\begin{aligned}&S:= \{ u_t+uu_x+vu_y+wu_z+p_x-\left( \underline{u_{xx}}+u_{yy}+u_{zz}\right)&= 0,\\&v_t+uv_x+vv_y+wv_z+p_y-\left( \underline{v_{xx}}+v_{yy}+v_{zz}\right)&= 0,\\&w_t+uw_x+vw_y+ww_z+p_z-\left( \underline{w_{xx}}+w_{yy}+w_{zz}\right)&= 0,\\&\underline{u_x}+v_y+w_z&= 0\}. \end{aligned}$$

A differential Thomas decomposition for S is given by the one system

$$\begin{aligned}S\cup \left\{ \ 2u_yv_x+2u_zw_x+2v_zw_y+u_x^2+v_y^2+w_z^2+\underline{p_{xx}}+p_{yy}+p_{zz}=0 \right\} ,\end{aligned}$$

where the Poisson pressure equation is added to S. In particular, the Thomas decomposition of S does not contain any inequation. A combinatorial calculation shows that the differential counting polynomial of the incompressible Navier–Stokes equations is \(\infty ^{\ell ^3+\frac{11}{2}\ell ^2+\frac{17}{2}\ell +4}\).

4.6 Examples

To transform a differential equation into an equation for a single power series coefficient, we define the partial map \(\rho :F\{U\}\rightarrow {\mathbb {C}}[G]\) as additive, multiplicative, mapping \(u^{(j)}_{\mu }\) to \(g^{(j)}_{\mu }\), and mapping any meromorphic \(f\in F\) to \(f(\zeta )\in {\mathbb {C}}\) if it has no pole in \(\zeta \).

We call the following the postponing of a differential equation \(p\in F\{U\}\): Replace p by its first derivatives \(\{\partial _{x_1}p,\ldots ,\partial _{x_n}p\}\) and \(\rho (p)\); this does not change the solution set.

In the following example, there is a power series coefficient that can be chosen arbitrarily except for a countable infinite exceptional set for a solution to exist. This exceptional set corresponds to the indeterminate \(\aleph _0\) in the differential counting polynomial. In particular, there exists a set of differential equations for which the indeterminate \(\aleph _0\) appears in the differential counting polynomial. This countable exceptional set carries over from the set of formal power series solutions to the set analytical solutions, as all formal power series solutions in this example have a positive radius of convergence. The author did not find a similar set of differential equations which describes natural phenomena or appears in the scientific literature.

Example 4.8

Let \(U=\{u^{(1)},u^{(2)}\}\), \(\Delta =\{\partial _t\}\), \(F={\mathbb {C}}(t)\), and < the orderly ranking with \(u^{(1)}>u^{(2)}\). We show the following. For all \(\ell \ge 1\)

$$\begin{aligned} \bar{c}(S)=c(S)(\ell )=\infty ^3-\infty ^2+\infty -\aleph _0 \end{aligned}$$

for formal power series solutions of \(S:=\{p:=u^{(2)}u^{(1)}_1-u^{(1)}+\frac{1}{t}=0, u^{(2)}_2=0\}\) centered around \(\zeta \in {\mathbb {C}}\setminus \{0\}\). Each of these solutions is locally convergent and S has no solutions centered around 0.

Use the ansatz \(u^{(1)}(t)=\sum _{i=0}^\infty g^{(1)}_i\frac{(t-\zeta )^i}{i!}\) and \(u^{(2)}(t)=\sum _{i=0}^\infty g^{(2)}_i\frac{(t-\zeta )^i}{i!}\). Adding \(g^{(2)}_0\not =0\) to S yields \(T:=\{p = 0, u^{(2)}_2 = 0, g^{(2)}_0 \not =0 \}\). It has \(\ell \)th differential counting polynomial \(c(T)(\ell )=\infty ^3-\infty ^2\) for every order \(\ell \ge 1\). This follows by means of the proof of Theorem 4.6 on p. 17; the inequation \(g^{(2)}_0 \not =0\) ensures that the initials of the derivatives of p are non-zero after applying \(\rho \).

The system \(S\cup \{g^{(2)}_0=0\}\), which is complementary to the previously treated system \(S\cup \{g^{(2)}_0\not =0\}\), is equivalent to

$$\begin{aligned}&S_1:=\{\partial _tp = u^{(2)}u^{(1)}_2+(u^{(2)}_1-1)u^{(1)}_1-\frac{1}{t^2}&= 0,&u^{(2)}_2&=0, \\&g^{(1)}_0-\frac{1}{\zeta }&=0,&g^{(2)}_0&=0\}, \end{aligned}$$

by postponing p. This system \(S_1\) belongs to the family

$$\begin{aligned} S_k:=\{ q_k:=u^{(2)}u^{(1)}_{k+1}+(ku^{(2)}_1-1)u^{(1)}_k+(-1)^{k}\frac{k!}{t^{k+1}}&= 0,&u^{(2)}_2 = 0,\\ (ig^{(2)}_1-1)g^{(1)}_i+(-1)^i\frac{i!}{\zeta ^{i+1}}&= 0&\forall \ 0\le i<k,\\ {\textstyle \prod _{i=1}^{k-1}(ig^{(2)}_1-1)}&\not =0,&g^{(2)}_0 =0 \} \end{aligned}$$

of systems. Here \(q_k\) results from differential reduction of \(\partial _t^kp\) by \(u^{(2)}_2\). After application of \(\rho \) and reduction with elements in \(S_k\), the differential equations \(q_k\) yield \((kg^{(2)}_1-1)g^{(1)}_k+(-1)^{k}\frac{k!}{\zeta ^{k+1}}\). To ensure a non-zero initial, we add \((kg^{(2)}_1-1)\not =0\) to \(S_k\). Then, postponing \(q_k\), which after reduction by \(u^{(2)}_2\) results in \(q_{k+1}\), yields the system \(S_{k+1}\). Complementary, when adding \(kg^{(2)}_1-1=0\) to \(S_k\), the system is inconsistent, since reducing \(\partial _tq_k\) by \(u^{(2)}_2\) results in \(q_{k+1}\). Then

$$\begin{aligned} \rho (q_{k+1})=g^{(2)}_0g^{(1)}_{k+2}+(kg^{(2)}_1-1)g^{(1)}_{k+1}+(-1)^{k+1}\frac{(k+1)!}{\zeta ^{k+2}}=0 \end{aligned}$$

yields the contradiction \((-1)^{k+1}\frac{(k+1)!}{\zeta ^{k+2}}=0\) by using the relations \(g^{(2)}_0=0\) and \(kg^{(2)}_1-1=0\).

Study the remaining system \(S_\infty :=\bigcup _{i=1}^\infty S_i\). The equations \((kg^{(2)}_1-1)g^{(1)}_k+(-1)^k\frac{k!}{\zeta ^{k+1}}=0\) make p superfluous. Furthermore, \(g^{(2)}_1\) cannot equal \(\frac{1}{k}\) for any \(k\in {\mathbb {Z}}_{\ge 1}\). Thus, there exists a countable infinite set of exceptional values for the power series coefficient \(g^{(2)}_1\) for which no solution exists. This results in

$$\begin{aligned}&T_\infty := \{ u^{(2)}_2 =0, \quad g^{(2)}_0&= 0,&&\\&(kg^{(2)}_1-1)g^{(1)}_k+(-1)^k\frac{k!}{\zeta ^{k+1}}&=0&\forall \ k\in {\mathbb {Z}}_{\ge 0},&\\&kg^{(2)}_1-1&\not =0&\forall \ k\in {\mathbb {Z}}_{\ge 1}\}.&\\ \end{aligned}$$

Hence, \({\mathfrak {Sol}}_\zeta (S)={\mathfrak {Sol}}_\zeta (T)\uplus {\mathfrak {Sol}}_\zeta (T_\infty )\).

For order \(\ell =0\), this system has one solution \(\{g^{(1)}_0=\frac{1}{\zeta }, g^{(2)}_0=0\}\) and thus its differential counting polynomial is 1. Its solution set is disjoint with that of T, which has differential counting polynomial \(\infty ^2-\infty \). Thus, the zeroth differential counting polynomial is \(\infty ^2-\infty +1\) for \(\ell =0\). Now assume \(\ell \ge 1\). The only choice in the special case system \(T_\infty \) is for \(g^{(2)}_1\) and it may be chosen freely in \({\mathbb {C}}\setminus \left\{ \left. \frac{1}{k}\right| k\in {\mathbb {Z}}_{\ge 1}\right\} \). Thus, \(c(T_\infty )=\infty -\aleph _0\). This implies that the counting sequence of S is

$$\begin{aligned} c(S)=l\mapsto {\left\{ \begin{array}{ll} \infty ^3-\infty ^2+\infty -\aleph _0, &{} \ell \ge 1\\ \infty ^2-\infty +1, &{} \ell =0. \end{array}\right. } \end{aligned}$$

These exceptional values for \(g^{(2)}_1\) correspond to the indeterminate \(\aleph _0\) in the differential counting polynomial.

All formal power series solutions of this example converge. This is implied for the ones of T by Riquier’s Existence Theorem [18]. For system \(T_\infty \), the solutions of \(u^{(2)}\) are lines and the radius of convergence for the formal power series solutions of \(u^{(1)}\) is \(|\zeta |\) by the ratio test:

$$\begin{aligned} \left| \frac{g^{(1)}_{k+1}}{(k+1)g^{(1)}_k}\right| =\left| \frac{kg^{(2)}_1-1}{(k+1)g^{(2)}_1-1}\right| \cdot \left| \frac{1}{\zeta }\right| \longrightarrow \left| \frac{1}{\zeta }\right| , k\rightarrow \infty \end{aligned}$$

The following example demonstrates that the additional information contained in the differential counting polynomial can be used to decide that a symbolic solver of differential equations did not find all solutions.

Example 4.9

Let \(U=\{u^{(1)},u^{(2)}\}\), \(\Delta =\{\partial _t\}\), \(F={\mathbb {C}}\), and < the orderly ranking with \(u^{(1)}>u^{(2)}\). We show the following. For all \(\ell \ge 1\)

$$\begin{aligned} \bar{c}(S)=c(S)(\ell )=\infty ^{\ell +2}-\infty ^{\ell +1}+(\ell +1)\infty ^\ell -\ell \infty ^{\ell -1} \end{aligned}$$

for formal power series solutions of \(S:=\{p:=u^{(2)}u^{(1)}_1-u^{(1)}=0\}\) centered around zero. The dimension polynomial is \(\ell +2\) (using Theorem 4.5 and the Low Power Theorem [11, IV.§15]).

Maple’s dsolve [1] returns an arbitrary \(u^{(2)}(t)\) and

$$\begin{aligned} u^{(1)}(t)=a\cdot e^{\int _0^t\frac{1}{u^{(2)}(h)}\mathrm {d}h} \end{aligned}$$

for a constant a. This set of solutions depends on \(\ell +2\) generically arbitrary constants up to order \(\ell \), in accordance with the dimension polynomial. The zeroth power series coefficient of \(u^{(2)}(t)\) cannot be zero, as otherwise the integral does not exist. Thus, Maple’s dsolve finds \(\infty ^{\ell +2}-\infty ^{\ell +1}\) solutions up to order \(\ell \) and a subset of the solutions with \(\ell \)th counting polynomial \((\ell +1)\infty ^\ell -\ell \infty ^{\ell -1}\) is not found. The dimension polynomial does not account for these additional solutions, some of which are analytic.

Now we show the claims from above. Use the ansatz \(u^{(1)}(t)=\sum _{i=0}^\infty a_i\frac{t^i}{i!}\) and \(u^{(2)}(t)=\sum _{i=0}^\infty b_i\frac{t^i}{i!}\). Let

$$\begin{aligned} \rho : {\mathbb {C}}\{U\}\rightarrow {\mathbb {C}}[a_i,b_i|i\in {\mathbb {Z}}_{\ge 0}]: u^{(1)}_i\mapsto a_i, u^{(2)}_i\mapsto b_i. \end{aligned}$$

Adding \(b_0\not =0\) to S yields \(T:=\{p = 0, b_0 \not =0\}\) with \(\ell \)th differential counting polynomial \(c(T)(\ell )=(\infty -1)\infty ^{\ell +1}\) for every order \(\ell \ge 1\).

Complementary, the system \(\{p=0, b_0=0\}\) is equivalent to \(S_1:=\{ \partial _tp=0, a_0=0, b_0=0 \}\) by postponing p. It is part of the family

$$\begin{aligned}&S_k:=\{ \partial _t^kp = u^{(2)}u^{(1)}_{k+1}+(ku^{(2)}_1-1)u^{(1)}_k+{\textstyle \sum _{i=2}^k\left( {\begin{array}{c}k\\ i\end{array}}\right) u^{(2)}_iu^{(1)}_{k+1-i}}&= 0, \\&a_0 = \cdots = a_{k-1} = b_0&=0, \\&{\textstyle \prod _{i=1}^{k-1}(ib_1-1)}&\not =0 \}&\end{aligned}$$

of systems. Consider the initial of the equation \(\rho (\partial _t^kp)\), which is equal to \((kb_1-1)a_k\) after reduction in \(S_k\). Adding its initial \((kb_1-1)\not =0\) to \(S_k\), and postponing \(\partial _t^kp\) results in the system \(S_{k+1}\). Complementary, adding \((kb_1-1)=0\) to \(S_k\) and postponing \(\partial _t^kp\) yields the system

$$\begin{aligned}&T_k:=\{ \partial _t^{k+1}p&= 0, \\&a_0 = \cdots = a_{k-1}&=0, \\&b_0 = kb_1-1&=0 \}. \end{aligned}$$

The inequations from \(S_k\) are superfluous in \(T_k\) because of the equation \(kb_1-1=0\). The equation \(\rho (\partial _t^{k+1+j}p)\) reduces to \(\frac{1}{k}a_{k+1+j}+\left( {\begin{array}{c}k+1+j\\ 2\end{array}}\right) b_2a_{k+j}\) in the context of \(T_k\) for all \(j\in {\mathbb {Z}}_{\ge 0}\). This reduced form has the leader \(a_{k+1+j}\) for all \(j\in {\mathbb {Z}}_{\ge 0}\); there is no constraint for \(a_k\).

Consider the remaining system \(T_\infty :=\bigcup _{i=1}^\infty S_i\). The equations \(a_k=0\) for all \(k\ge 0\) combine to the differential equation \(u^{(1)}=0\); this makes the differential equation p superfluous. Furthermore, \(b_1\) is not allowed to be of the form \(\frac{1}{i}\) for any \(i\in {\mathbb {Z}}_{\ge 1}\). Summing up, the system \(T_\infty :=\{u^{(1)}=0,b_0=0,ib_1\not =1\ \forall i\in {\mathbb {Z}}_{\ge 1}\}\) describes these remaining solutions.

We discuss the \(\ell \)th differential counting polynomials for \(\ell \ge 1\) of the sets of solutions of \(T_\infty \) and \(T_k\), \(k\ge 1\). These systems have disjoint sets of solutions in orders \(\ell \ge 1\), since \(b_1\) takes different values. The \(\ell \)th differential counting polynomial of \(T_k\) for \(k\le \ell \) is \(\infty ^\ell \), since the values for the indeterminates \(a_k,b_2,\ldots ,b_\ell \) are freely choosable and the other values are fixed. In the union \(\biguplus _{k>\ell ,k=\infty }{\mathfrak {Sol}}_0(T_k)_{\le \ell }\), the value for \(b_1\) can be freely chosen except for the \(\ell \) values \(\frac{1}{1},\ldots ,\frac{1}{\ell }\). Then, the indeterminates \(b_2,\ldots ,b_\ell \) have no constraint and the indeterminates \(a_i\) are uniquely determined. Thus,

$$\begin{aligned} c\Big (\biguplus _{k>0,k=\infty }{\mathfrak {Sol}}_0(T_k)_{\le \ell }\Big )&=\sum _{1\le k\le \ell }c\big ({\mathfrak {Sol}}_0(T_k)_{\le \ell }\big ) +c\Big (\biguplus _{k>\ell ,k=\infty }{\mathfrak {Sol}}_0(T_k)_{\le \ell }\Big ).\\&=\ell \cdot \infty ^\ell +(\infty -\ell )\cdot \infty ^{\ell -1}\\&=(\ell +1)\infty ^\ell -\ell \cdot \infty ^{\ell -1} \end{aligned}$$

Adding this \(\ell \)th counting polynomial to the one of T results in \(\infty ^{\ell +2}-\infty ^{\ell +1}+(\ell +1)\infty ^\ell -\ell \infty ^{\ell -1}\), as claimed above.

Riquier’s Existence Theorem [18] implies the convergence for the power series solutions of system T for analytical initial conditions. System \(T_\infty \) gives the zero power series for \(u^{(1)}\), which converges and only restricts the choice for the first two power series coefficients of \(u^{(2)}\), hence \(u^{(2)}\) can be chosen to converge. The solutions of the systems \(T_k\) can diverge even for analytical initial conditions. For example, consider system \(T_1\) and prescribe \(b_0=0, b_1=1, b_2=1, b_i=0\) for all \(i\ge 3\). By the ratio test, the radius of convergence of the solution for \(u^{(1)}\) is zero, as

$$\begin{aligned} \left| \frac{a_{k+1}}{(k+1)a_k}\right| =\frac{k-1}{k}\left| \frac{\sum _{i=2}^k\left( {\begin{array}{c}k\\ i\end{array}}\right) \frac{b_{i+1}}{i+1}a_{k+1-i}}{\sum _{i=2}^k\left( {\begin{array}{c}k\\ i\end{array}}\right) b_ia_{k+1-i}} +\frac{k}{2}b_2\right| =\frac{k-1}{2} \longrightarrow \infty \end{aligned}$$

for \(k\rightarrow \infty \). The analytical initial condition \(b_0=0, b_1=1, b_2=0, b_i=i!\), for \(i\ge 3\), gives 1 as radius of convergence by a similar computation.

5 Proofs

This section proves the theorems of the previous sections.

5.1 Proof of Theorem 3.5

By abuse of notation, let c denote the counting polynomials for subsets in \({\mathbb {C}}^k\) for all \(1\le k\le n\).

Proof of existence

Let \(S\subset {\mathbb {C}}[y_1,\ldots ,y_n]\) be a simple algebraic \(\sigma \)-system. Furthermore, let \(\tau (S_{y_i})\) be the degree of the equation if \(S_{y_i}\) is a singleton of an equation, \(\tau (S')=\prod _{p\in S'}\deg _{y_i}(p)\) if \(S_{y_i}\) is a finite set of inequations, and \(\tau (S_{y_i})=\infty -\aleph _0\) if \(S_{y_i}\) is a countably infinite set of inequations. Then, the product \(\prod _{i=1}^n \tau (S_{y_i})\) is a counting polynomial. The correctness of this formula follows from the fibration structure of simple systems as discussed in [16], which also holds for simple \(\sigma \)-systems. \(\square \)

Write \(T:={\mathfrak {Sol}}(S)\) and \(\overline{T}\) for its Zariski closure. Let \(\pi :{\mathbb {C}}^n\rightarrow {\mathbb {C}}^{n-1}\) be the projection to the first \(n-1\) components. The projected set \(\pi (T)\) is equal to the solution set of the simple \(\sigma \)-system \(S_{<y_n}\) in \({\mathbb {C}}[y_1,\ldots ,y_{n-1}]\).

Proof of uniqueness

For systems (instead of \(\sigma \)-systems), the claim is shown in [16, Prop. 3.3]; in this case, Lazard’s Lemma implies that the degree of the algebraic counting polynomial is equal to the dimension of the set of solutions.

In this proof, we can ignore sets of lower dimension, since any counting polynomial of such a set is of lower degree and we can proceed by an induction on \(\dim (T)\). Any partition of T into solution sets of algebraic \(\sigma \)-systems of the same dimension is finite. Such a finite partition does not change the degree and leading coefficient of the counting polynomial, by the same arguments as in step 3 of the proof of [16, Prop. 3.3]. Thus, in the following, we can always assume that a set is suitably partitioned into a disjoint union of sets.

The claim is clear for \(n=1\). We show the claim for the dimension n of the surrounding space under the assumption that it is shown for dimensions 0 up to \(n-1\). The crux of the proof is that only axiom (3.1) in Definition 3.1 allows to increase this dimension.

By the assumption on \(n-1\), the algebraic counting polynomials of the two projections \(\pi (T)\subseteq \pi (\overline{T})\) have the same degree, say d, and leading coefficients, say a, as their Zariski closures coincide.

As first case consider that \(S_{y_n}\) is a set of inequations. By Definition 3.1.(3.1), any algebraic counting polynomial of T is an algebraic counting polynomial of \(\pi (T)\) multiplied by \(\infty -b\) for \(b\in {\mathbb {Z}}[\aleph _0]\). In particular, any leading coefficient is a and any degree is \(d+1\). Furthermore, \(\overline{T}=\pi (\overline{T})\times {\mathbb {C}}\) has a unique counting polynomial, which is \(c(\pi (\overline{T}))\cdot \infty \) and also has leading coefficient a and degree \(d+1\).

As second case consider that \(S_{y_n}\) is an equation. In this case we do an induction over \(\dim (T)\). The claim is clear for \(\dim (T)=0\), so assume that it is shown for all dimensions from 0 to \(\dim (T)-1\).

On the one hand, by Definition 3.1.(3.1), the degree of any counting polynomial of T is again d and any leading coefficient is \(a\cdot \deg _{y_n}(S_{y_n})\).

On the other hand, consider \(\overline{T}\). The map \(\pi \) makes \(\overline{T}\) an \(\deg _{y_n}(S_{y_n})\)-sheeted cover of \(\pi (\overline{T})\). Denote by \(R\subseteq \pi (\overline{T})\) the corresponding set of ramification points and by \(U:=\pi (\overline{T})\setminus R\) the set of unramified points. To apply Definition 3.1.(3.1), one needs to partition \(\overline{T}\) into (a refinement of) \(\pi ^{-1}(R)\) and \(\pi ^{-1}(U)\); thus, any algebraic counting polynomial needs to be defined using this partition. As U and R are locally closed, their algebraic counting polynomials exist and are unique. The Zariski closures of U and \(\pi (\overline{T})\) coincide, so by induction on n the leading coefficient of c(U) is a and \(\deg _\infty (c(U))=d\). By Definition 3.1.(3.1), the algebraic counting polynomial of \(\pi ^{-1}(U)\) has the same degree and leading coefficient as that one of T, as \(\pi ^{-1}(U)\) is an unramified \(\deg _{y_n}(S_{y_n})\)-sheeted cover of U and the set \(\pi ^{-1}(R)\) is of lower dimension than \(\overline{T}\). \(\square \)

5.2 Proof of Theorem 3.6

The proof of Theorem 3.2 is given in [16, Cor. 3.4]. The following two lemmas directly generalize this proof to showing Theorem 3.6. We call a set \(W\subset {\mathbb {C}}^n\) elementarily well-fibered if either \(n=1\) and W is constructible or \(n>1\), \(\pi (W)\subseteq {\mathbb {C}}^{n-1}\) is elementarily well-fibered, and all fibers of \(\pi ^{-1}(\{w\})\) for \(w\in \pi (W)\) are constructible with equal algebraic counting polynomials. They admit an algebraic counting polynomial in \({\mathbb {Z}}[\infty ]\) by definition.

Lemma 5.1

Let V be a well-fibered set. Then there exists a finite partition \(V=\biguplus _{i=1}^kW_i\) of V into elementarily well-fibered sets \(W_i\).

Proof of uniqueness

The claim clearly holds for \(n=1\). The only one of the five axioms for the algebraic counting polynomial that allows one to increase the dimension is axiom (3.1). In general, one needs to partition V before applying axiom (3.1), but this partition needs to be finite, as otherwise axiom (3.1) is not applicable to recombine the resulting algebraic counting polynomials. Elementarily well-fibered sets are exactly the sets for which axiom (3.1) is applicable without additional partitioning. \(\square \)

Lemma 5.2

Let V be a well-fibered set. Then, the algebraic counting polynomial of V is unique.

Proof of uniqueness

The proof of [16, Prop. 3.3] regarding the uniqueness of algebraic counting polynomials holds for well-fibered sets. One only needs to replace a partition into solution sets of simple systems with a partition into elementarily well-fibered sets, which exists by Lemma 5.1.\(\square \)

5.3 Proof of Theorem 4.1

Transform the algebraically restricted system of differential equations S by keeping all equations and inequations in \({\mathbb {C}}[G]\) and apply \(\rho \) (cf. p. 10) to the differential equations and all their (iterated) derivatives. Call the resulting set Q; it consists of infinitely many equations and inequations in \({\mathbb {C}}[G]\) and has the same set of solutions as S. Write \(G=\{\overline{g_1},\overline{g_2},\ldots \}\) ordered by the ranking, i.e., \(\overline{g_i}<\overline{g_{i+1}}\) for all i. Note that \(Q\cap {\mathbb {C}}[\overline{g_1},\ldots ,\overline{g_i}]\) is finite for all \(i\in {\mathbb {Z}}_{>0}\).

Let \(\overline{g_j}\) be the largest element in G of order \(\ell \). Define the set \(L_0:=\textsf {Decompose}(Q\cap {\mathbb {C}}[\overline{g_1},\ldots ,\overline{g_j}])\) of simple systems, where Decompose is the Thomas decomposition algorithm from [2]. Iteratively, define the sets \(L_k\) of simple systems by making

$$\begin{aligned} \left\{ \textsf {Decompose}(T\cup (Q\setminus {\mathbb {C}}[\overline{g_1},\ldots ,\overline{g_{j+k-1}}])\cap {\mathbb {C}}[\overline{g_1},\ldots ,\overline{g_{j+k}}])|T\in L_{k-1}\right\} \end{aligned}$$

comprehensive (cf. Sect. 2) with respect to \(\overline{g_j}\) for each \(k\in {\mathbb {Z}}_{>0}\). Let \(L_k':=\{T\cap {\mathbb {C}}[\overline{g_1},\ldots ,\overline{g_j}]\mid T\in L_k\}\) for each \(k\in {\mathbb {Z}}_{\ge 0}\). The simple systems in \(L_k'\) have disjoint sets of solutions, as \(L_k\) is comprehensive w.r.t. \(\overline{g_j}\).

For any power series which is not a solution of the input system S, there exists a k large enough such that it is no longer the solution of any system in \(L_k\), as each constraint in Q is taken into account at some step.

Next we show that equations stabilize by looking at ideals. Let \(J_k:=\bigcap _{T\in L_k'}{\mathcal {I}}(T)\) be an ideal in the Noetherian ring \({\mathbb {C}}[G]_{\le \ell }\) for each \(k\in {\mathbb {Z}}_{\ge 0}\). This ideal is equal to intersecting \({\mathbb {C}}[G]_{\le \ell }\) with the vanishing ideal of \(Q\cap {\mathbb {C}}[\overline{g_1},\ldots ,\overline{g_{j+k}}]\). In particular, this ascending chain of ideals does stabilize after a finite number \(k'\) of steps. This stable ideal is the vanishing ideal of all power series solutions truncated at order \(\ell \).

By construction for each simple system \(T_{k+1}\in L_{k+1}'\), there is a unique simple system \(T_k\in L_k'\) with \({\mathfrak {Sol}}(T_{k+1})\subseteq {\mathfrak {Sol}}(T_k)\); if additionally \({\mathcal {I}}(T_{k+1})={\mathcal {I}}(T_k)\), then call \(T_{k+1}\) the (unique) heir of \(T_k\). Define a successor as an element in the transitive hull of heir.

As \(J_{k'}\) is a radical ideal in the Noetherian ring \({\mathbb {C}}[G]_{\le \ell }\), it has a finite prime decomposition. There is a minimal \(L_k''\subseteq L'_{k}\) such that \(J_{k'}=\bigcap _{T\in L_k''}{\mathcal {I}}(T)\) for each \(k\ge k'\). By increasing \(k'\) we may assume that the cardinality of each \(L_k''\) is equal for all \(k\ge k'\). In particular, each \(T_k\in L_k''\) has an heir in \(L_{k+1}''\).

A closer look at the algebraic Thomas decomposition algorithm Decompose reveals that a system and all its successors do not only have equal ideals but also equal sets of equations. In particular, a system and its heir only differ in their set of inequations. We can slightly adapt the algebraic Thomas decomposition algorithm Decompose such that the simple systems (and the candidate simple systems \(S_T\)) allow more than one inequation with the same leader, as long as the conditional gcd of these inequations with the same leader have no common zero with the system. This adaption changes nothing of the previous discussion. However, now the inequations of a simple system are a subset of the inequations of its heir, and thus the union of any system in \(L_{k'}''\) with all its successors is a simple algebraic \(\sigma \)-system.

This results in a finite set of algebraic \(\sigma \)-systems having truncated solutions that are dense in the truncated solutions of S. The complement of this dense set is described by a countable set of systems. Continue with these systems inductively. The ideals of these complementary systems are strictly larger than the previous ideals. In particular, descending chains of these systems are finite in length. Hence, the number of algebraic \(\sigma \)-systems remains countable. \(\square \)

5.4 Proof of Theorem 4.5

The claim for the \(\ell \)th differential counting polynomial is a corollary to Theorem 3.5. Thereby, we can assume without loss of generality that the set of solutions \({\mathfrak {Sol}}_\zeta (I)_{\le \ell }\) up to order \(\ell \) is constructible. Now, the claim follows directly from the definition of the differential dimension function \(\Omega _I:\ell \mapsto \dim (F\{U\}_{\le \ell }/I_{\le \ell })\) and that the dimension coincides with the degree of the algebraic counting polynomial. The formula for the coefficient also follows from the proof of Theorem 3.5; we do not need to consider the degrees of the (quasilinear) derivatives of the equations.

The claim for the differential counting polynomial follows, as the dimension polynomial \(\omega _I\) ultimately coincides with \(\Omega _I\).

5.5 Proof of Theorem 4.6

We prove this theorem by creating suitable simple algebraic systems \(S_{\le \ell }\subset {\mathbb {C}}[G]_{\le \ell }\), which describe the formal power series solutions of S around a point \(\zeta \) truncated at order \(\ell \).

For this, define \(\overline{S}\) by applying \(\rho \) (cf. p. 10) to the equations in S and all their reductive prolongations (cf. [2, §3]). Then, define \(S_{\le \ell }:=\overline{S}\cap {\mathbb {C}}[G]_{\le \ell }\).

It is straightforward that \(S_{\le \ell }\) is a simple algebraic system in \({\mathbb {C}}[G]_{\le \ell }\), e.g. derivatives are square-free, as they are quasilinear and the initial of a derivative is the separant of the original equation.

Next, we show that the formal power series solutions of S around a point \(\zeta \) truncated at order \(\ell \) are the same as those of S, i.e., \({\mathfrak {Sol}}_\zeta (S)_{\le \ell }={\mathfrak {Sol}}_\zeta (S_{\le \ell })_{\le \ell }\). This would be clear if \(\overline{S}\) contained all derivatives of equations in S and not only the reductive prolongations. However, the non-reductive prolongations are redundant, as S is involutive (cf. [2, 3.5]).

Finally, the existence proof of Theorem 3.5 on p. 14 allows to read off the counting polynomial from \(S_{\le \ell }\): The number of free variables is equal to the value of the differential dimension function at \(\ell \) (and to the value of the dimension polynomial for \(\ell \) large enough). Furthermore, one needs to multiply the degrees of the equations to get the coefficient; these degrees are one for all derivatives, and thus one is left with the degrees of the equations in S.

The uniqueness follows from Theorem 4.3, as no \(\aleph _0\) appears. \(\square \)