Christoph Weidenbach
email: weidenb@mpi-inf.mpg.de

The Challenge of Unifying Semantic and Syntactic Inference Restricions

While syntactic inference restrictions don't play an important role for SAT, they are an essential reasoning technique for more expressive logics, such as first-order logic, or fragments thereof. In particular, they can result in short proofs or model representations. On the other hand, semantically guided inference systems enjoy important properties, such as the generation of solely non-redundant clauses. I discuss to what extend the two paradigms may be unifiable.

Introduction

In [START_REF] Weidenbach | Do portfolio solvers harm?[END_REF] I discussed the differences between simple-syntactic portfolio solvers and sophisticatedsematic portfolio solvers. In this paper I present the challenges in combining a solver based on syntactic inference restrictions with a solver based on the semantic guidance of inferences. More concretely, I investigate the differences between CDCL-style solvers building a partial model assumption and solvers based on ordering and selection restrictions on inferences.

NP-Complete Problems

The prime calculus for SAT is CDCL (Conflict Driven Clause Learning) [START_REF] João | Grasp -a new search algorithm for satisfiability[END_REF][START_REF] Moskewicz | Chaff: Engineering an efficient sat solver[END_REF][START_REF]Handbook of Satisfiability[END_REF][START_REF] Christian Blanchette | A verified SAT solver framework with learn, forget, restart, and incrementality[END_REF]. The calculus can be viewed as a resolution variant where resolution inferences are selected via partial model assumptions. The CDCL calculus operated on a five tuple (M, N, U, k, C) where M is a sequence of literals representing the current model assumption, called the trail, N the clause set under consideration, U a set of learned clauses, i.e., clauses derived via resolution, k the number guessed/decided literals in M , called the decision level, and C a clause that is if no conflict has occurred yet, some non-empty clause representing a found conflict, or ⊥ in case of an overall contradiction. Consider the clause set

N = {P ∨ Q ∨ R, ¬R ∨ S, ¬S ∨ P ∨ Q, . . .}
where a CDCL run starting from the empty trail may result in ( ; N ; ∅; 0; )

⇒ * CDCL ([¬P 1 ¬Q 2 R P ∨Q∨R S ¬R∨S ]; N ; ∅; 2; ¬S ∨ P ∨ Q)
where the literals ¬P , ¬Q were decided (guessed) at decision levels 1, 2, respectively; R is the propagated via the clause P ∨ Q ∨ R; S is propagated via ¬R ∨ S and finally in the partial assignment [¬P 1 ¬Q 2 R P ∨Q∨R S ¬R∨S ] the clause ¬S ∨ P ∨ Q is false. The conflict is solved by resolving the false clause with clauses propagating on the trail. First with ¬R ∨ S resulting in ¬R ∨ P ∨ Q and then with P ∨ Q ∨ R resulting in P ∨ Q. Now this clause is learned yielding the new CDCL state

⇒ * CDCL ([¬P 1 Q P ∨Q ]; N ; {P ∨ Q}; 1;
). Most importantly, the new clause P ∨ Q is non-redundant, i.e., it is not implied by smaller clauses from N , where the ordering is a lifting of the literal ordering generated by the trail [START_REF] Alagi | NRCL -A model building approach to the bernaysschönfinkel fragment[END_REF][START_REF] Fiori | Scl -clause learning from simple models[END_REF]. Propositional non-redundancy is itself an NP-complete property. Hence, a polynomial time procedure generates a clause that enjoys an NP-complete property. This has several immediate consequence: (i) termination (ii) the approach of forgetting clauses works. Note that since only non-redundant clauses are learned by CDCL, a forgotten clause that has become redundant will not be generated a second time. Hence, learning plus forgetting can be seen as an efficient way to getting rid of redundant clauses.

Please recall, the classical first-order notion of redundancy means "not needed to find a proof or model". Therefore, a redundant clause can be deleted. In the superposition or ordered resolution context this abstract definition is instantiated with "not implied by smaller clauses". However, in the context of SAT, redundancy is often defined as a synonym for "satisfiability preserving". So in the context of many SAT related papers redundant clauses must not be removed, in general, or completeness is lost. These two notions of redundancy must not be confused and I stick here to the classical first-order notion.

The prerequisites for learning non-redundant clauses are twofold:

1. Propagation needs to be exhaustive.

2. Conflict detection needs to be eager.

The number of literals of a SAT problem is typically small compared to the respective clause set size. Therefore, exhaustive propagation in SAT is not an issue, as well as the detection of conflicts, i.e., false clauses. Surprisingly, what holds for SAT, does not hold for NP-complete problems, in general. It seems that the language of propositional logic is a nice compromise between expressivity and the efficiency of propagation.

Consider the NP-complete problem of testing satisfiability of a system of linear arithmetic inequations over the integers [START_REF] Karp | Reducibility among combinatorial problems[END_REF][START_REF] Papadimitriou | On the complexity of integer programming[END_REF]. The language of linear integer arithmetic is more succinct than propositional logic, i.e., the encoding of on integer variable x requires linearly many propositional variables, because the a priori bounds for solvability are simply exponential. Now consider a CDCL style procedure testing solvability of a LIA (Linear Integer Arithmetic) system of inequations [START_REF] Bromberger | Linear integer arithmetic revisited[END_REF]. Consider the example system

N = {1 -x -y ≤ 0, x -y ≤ 0, . . .}
and a CDCL-style run via CATSAT+ [START_REF] Bromberger | Linear integer arithmetic revisited[END_REF], where the partial model assumption is represented by simple bounds, i.e., inequations of the form x#c, c ∈ Z, # ∈ {<, >, ≤, ≥}.

( ; N ; ∅; 0; ) ⇒ * CATSAT+ ([x ≥ 5 1 y ≥ 6 1-x-y≤0
x ≥ 6 x-y≤0 . . .]; N ; ∅; 1; ) Obviously, the propagation does not terminate, except for a priori simply exponential bounds: if m is the number of inequations in N , n the number of different variables in N and a the maximal coefficient in N , then the problem has a solution iff -n • (m • a) 2m+1 ≤ x ≤ n • (m • a) 2m+1 for every variable x in N [START_REF] Papadimitriou | On the complexity of integer programming[END_REF]. Hence, there is currently no CDCL-style procedure known that does exhaustive propagation. Therefore, the learned clauses [START_REF] Bromberger | Linear integer arithmetic revisited[END_REF] are not non-redundant. The current state-of-the-art procedures don't us a CDCL-style approach but apply a relaxation of LIA to LRA (linear rational arithmetic) and use LRA solutions for a branch-and-bound approach. This general idea is complemented via simplifications and fast, sufficient tests for the existence of a solution [START_REF] Bradley | The Calculus of Computation -Decision Procedures with Applications to Verification[END_REF][START_REF] Kroening | Decision Procedures An Algorithmic Point of View[END_REF][START_REF] Bromberger | New techniques for linear arithmetic: cubes and equalities[END_REF][START_REF] Bromberger | A reduction from unbounded linear mixed arithmetic problems into bounded problems[END_REF].

NEXPTIME-Complete Problems

The same phenomenon that occurs at LIA, see Section 2, also shows up if the complexity is "slightly" increased from SAT to the satisfiability of the Bernays-Schoenfinkel (BS) fragment of first-order logic [START_REF] Bernays | Zum entscheidungsproblem der mathematischen logik[END_REF], which is NEXPTIME-Complete [START_REF] Plaisted | Complete problems in the first-order predicate calculus[END_REF]. For example, consider the following clause set [START_REF] Antonio | Proof systems for effectively propositional logic[END_REF]

N =                    1 : P (0, 0, 0, 0), 2 : ¬P (x 1 , x 2 , x 3 , 0) ∨ P (x 1 , x 2 , x 3 , 1), 3 : ¬P (x 1 , x 2 , 0, 1) ∨ P (x 1 , x 2 , 1, 0), 4 : ¬P (x 1 , 0, 1, 1) ∨ P (x 1 , 1, 0, 0), 5 : ¬P (0, 1, 1, 1) ∨ P (1, 0, 0, 0), 6 : ¬P (1, 1, 1, 1)                   
where a CDCL-style run, using ground literals for the partial model assumptions [START_REF] Fiori | Scl -clause learning from simple models[END_REF], will propagate all values of the 4-bit counter represented by P : ( ; N ; ∅; 0; ) ⇒ * SCL ([P (0, 0, 0, 0) 1 P (0, 0, 0, 1) 2 P (0, 0, 1, 0) 3 . . . P (1, 1, 1, 1) 2 ], N, ∅, 0, ¬P (

before detecting the conflict, where for the propagation justifications I used the clause numbers. Thus, there are exponentially many propagations, in general. Still, the clause set can be refuted in linearly many steps by starting with resolution steps between the clauses 2 -4: 2.2 Res 3.1 7 : ¬P (x 1 , x 2 , 0, 0) ∨ P (x 1 , x 2 , 1, 0) 7.2 Res 2.1 8 : ¬P (x 1 , x 2 , 0, 0) ∨ P (x 1 , x 2 , 1, 1) 8.2 Res 4.1 9 : ¬P (x 1 , 0, 0, 0) ∨ P (x 1 , 1, 0, 0) 9.2 Res 8.1 10 : ¬P (x 1 , 0, 0, 0) ∨ P (x 1 , 1, 1, 1) 10.2 Res 5.1 11 : ¬P (0, 0, 0, 0) ∨ P (1, 0, 0, 0) 11.2 Res 10.1 12 : ¬P (0, 0, 0, 0) ∨ P (1, 1, 1, 1) 12.1 Res 6.1 13 : ⊥. which corresponds to a standard ordering restriction on the P atoms, e.g., via a KBO, plus a respective selection strategy [START_REF] Bachmair | Rewrite-based equational theorem proving with selection and simplification[END_REF]. For example, for the first step the second literal out of clause 2 is maximal with respect to a KBO instance where 1 > KBO 0 and the first literal of clause 3 is selected.

In addition, for "practically relevant" instances of the BS fragment the situation is the same. We have shown [START_REF] Suda | On the saturation of yago[END_REF] that the YAGO [START_REF] Suchanek | Yago: a core of semantic knowledge[END_REF] fragment of BS can be effectively saturated by a variant of ordered resolution with chaining, whereas all model-guided approaches fail. Again for the reason that propagation with respect to millions of constants cannot be efficiently done, yet.

Unification

The two frameworks, syntactic inference restrictions and model-guided inferences cannot be easily combined. Obviously, since ordered resolution may generate redundant clauses, but model-guided inferences with exhaustive propagation and eager conflict detection do not, modelguided inferences cannot simulate resolution inferences. The resolution inferences in Section 3 refuting the counter encoding are not redundant. Still, they cannot be simulated by a CDCLstyle calculus [START_REF] Fiori | Scl -clause learning from simple models[END_REF] because it will immediately run into the exponentially many propagation steps and find a refutation of exponential size this way. It seems to be non-trivial and non-obvious how the two paradigms can be unified. If eager propagation is dropped, then model-guided inferences can simulate resolution [START_REF] Pipatsrisawat | On the power of clause-learning sat solvers with restarts[END_REF][START_REF] Fiori | Scl -clause learning from simple models[END_REF], however, in this case non-redundancy of learned clauses is lost, in general.


Sény Diatta
email: senydiatta@gmail.com

Guillaume Moroz

Marc Pouget

Reliable Computation of the Singularities of the Projection in R 3 of a Generic Surface of R 4

Computing efficiently the singularities of surfaces embedded in R 3 is a difficult problem, and most state-of-the-art approaches only handle the case of surfaces defined by polynomial equations. Let F and G be

y, z, t) = 0} be the surface they define. Generically, the surface M is smooth and its projection Ω in R 3 is singular. After describing the types of singularities that appear generically in Ω, we design a numerically well-posed system that encodes them. This can be used to return a set of boxes that enclose the singularities of Ω as tightly as required. As opposed to state-of-the art approaches, our approach is not restricted to polynomial mapping, and can handle trigonometric or exponential functions for example.

Introduction

Consider two real analytic functions F, G defined in R 4 and denote by M the smooth surface defined as the real common zeros of F and G. Let p be the projection map from M to R 3 along the direction (0, 0, 0, 1) and Ω the image of M by p. The goal of this paper is to take advantage of the structure of the singularities of Ω and to present a regular system allowing to isolate them efficiently. Computing the singularities of such surfaces is fundamental for the reliable visualization of surfaces, and for problems that arise in fields such as mechanical design, control theory or biology.

The modern theory of singularities started with Whitney, Thom and Mather and the classification of singularities is an active research domain since then. Most of the literature focus on the local case of germs of functions, and only more recently the case of multigerms, that is taking into account the interplay of several points in the source space at once, attracted more attention, see e.g. [START_REF] Sinha | Classification of multigerms (from a modern viewpoint)[END_REF] and references therein. Particularly relevant for our work is the case of functions from a surface to R 3 which is studied in [START_REF] Goryunov | Local invariants of mappings of surfaces into three-space[END_REF][START_REF] Hobbs | On the classification and bifurcation of multigerms of maps from surfaces to 3-space[END_REF][START_REF] Mond | On the classification of germs of maps from R 2 to R 3[END_REF].

Unfortunately, these classifications do not lead directly to algorithms computing explicitly the singularities associated to varieties. Still, in [START_REF] Delanoue | A numerical approach to compute the topology of the apparent contour of a smooth mapping from R 2 to R 2[END_REF], a numeric approach is presented for computing the apparent contour of a function from the plane to itself. In [START_REF] Imbach | Numeric and certified isolation of the singularities of the projection of a smooth space curve[END_REF], the authors proposed a reliable numeric algorithm to compute the singularities of the projection of smooth curves from R 3 to R 2 , using a so-called Ball system. We generalize this approach to compute the singularities of the projection of smooth surfaces from R 4 to R 2 .

After recalling some results from singularity and transversality theory in Section 2, we prove our first result on the types of singularities in Ω, the projection of a generic smooth compact surface, in Section 3. We prove in Section 4 that Equations (S-Ball) define a regular system that can be used to compute the set of singularities of Ω. Finally, in Section 5, we will illustrate our approach with the classical Whitney Umbrella, and with the computation of the singularities of a surface that cannot be handled by state-of-the-art method up to our knowledge.

Notation and main results

In the following, the surface M is a compact smooth 2-submanifold of R 4 defined by the zero locus of the C ∞ functions F and G. We denote by S compact the subset of mappings in C ∞ (R 4 , R 2 ) that implicitly define a compact surface. With the coordinates (x, y, z, t) on R 4 , we denote p : M → R 3 the projection along the taxis, and Ω is the image of M by p. We call a plane in R 4 vertical if it is parallel to the t-axis, that is it contains the vector (0, 0, 0, 1). The tangent plane P of M at a point q is the set of vectors orthogonal to both ∇F (q) = (∂ x F, ∂ y F, ∂ z F, ∂ t F )(q) and ∇G(q). Thus the tangent plane at q is vertical iff ∂ t F (q) = ∂ t G(q) = 0. We say that a property is generic if it is satisfied by a countable intersection of open dense sets of C ∞ mappings (see [4, §3.2.6]). The open sets we consider are given by the Whitney topology (as defined in [4, p.45] or [6, chap. II §3]) on the space of smooth maps C ∞ (R 4 ; R 2 ), restricted to S compact .

Our first result is a description of the generic singularities of Ω in terms of singularities of the projection map. We prove that Ω generically has only 3 kinds of singularities whose definition is given in [START_REF] Hobbs | On the classification and bifurcation of multigerms of maps from surfaces to 3-space[END_REF], and recalled in Definition 3.

Theorem 1. (Generic properties)

1. The surface defined by F = G = 0 is generically smooth. 2. The singularities of the projection in R 3 of a generic compact surface of R 4 is a curve C of double points having as singularities a discrete set of triple points and cross-caps.

To compute the curve C of double points, a naive approach consists in duplicating the last variable, as in Equation (S-dble) of Section 4.1. However, this leads to a system that is not regular near the cross-caps. Thus, such an approach is not suitable for numerical solvers such as path continuation or subdivision algorithms.

Our second result shows that the computation of the singular curve C can be reduced to solving the regular system (S-Ball) of 4 equations in 5 variables. We call this system the Ball system as in [START_REF] Imbach | Numeric and certified isolation of the singularities of the projection of a smooth space curve[END_REF] where the same approach was used for the projection of a space curve in the plane. We first define the operators S and D applied to a given smooth function A defined on R 4 .

S.A(x, y, z, c, r) = 1 2 (A(x, y, z, c + √ r) + A(x, y, z, c - √ r)) if r > 0 A(x, y, z, c) if r = 0, D.A(x, y, z, c, r) = 1 2 √ r (A(x, y, z, c + √ r) -A(x, y, z, c - √ r)) if r > 0 ∂tA(x, y, z, c) if r = 0.
We then define the Ball system as

S.F (x, y, z, c, r) = 0 S.G(x, y, z, c, r) = 0 D.F (x, y, z, c, r) = 0 D.G(x, y, z, c, r) = 0. (S-Ball)

Theorem 2. (Computation of the singularities)

Let M ⊂ R 4 be a compact surface solution of F = G = 0 that satisfies the generic properties of Theorem 1. Let C Ball be the curve solution of the system (S-Ball).

1. The points of C Ball are regular points of System (S-Ball).

The projection of C

Ball to R 3 is the singular locus C of Ω.
A direct corollary of this theorem is that one can enclose the curve of singularities of Ω using state-of-the-art numerical algorithms such as the one presented in [START_REF] Martin | Certified parallelotope continuation for one-manifolds[END_REF] for example.

Preliminaries

Before enumerating the different types of singularities that can appear on the projection in R 3 of a generic surface of R 4 , we recall some basic definitions on regularity and transversality theory.

Regular, critical and singular points Definition 1. (Regular and critical points of p)

-Regular point of p. A point q ∈ M is a regular point of p when its derivative has full rank, that is rank(dp) q = 2. This is equivalent to say that the tangent plane to M at q is not vertical. -Critical point of p. A point q ∈ M which is not a regular point of p is called a critical point of p. Equivalently the tangent plane at q is vertical i.e.

∂ t F (q) = ∂ t G(q) = 0.
Let P be a point of Ω, we say that a point q ∈ p -1 (P ) ⊂ M is a regular (resp. singular) pre-image of P , if q is a regular (resp. critical) point of p.

Definition 2. (Regular points of a variety or a system)

-Regular point of Ω. A point P ∈ Ω is a regular point of Ω if Ω is locally a 2-submanifold of R 3 , otherwise, it is a singular point of Ω.
-Regular solution of a system. A solution of a square system is regular if the Jacobian determinant does not vanish at this solution. When there are more variables than equations, one requires that the Jacobian matrix is full rank (i.e. the associated linear map is surjective) at the solution.

For a point P ∈ Ω with pre-images q i ∈ M, we denote P i the tangent plane of M at q i and Π i its image by p. We distinguish three types of singular points of Ω that are illustrated in Figure 1. -Double point. P ∈ Ω is a double point if it has two regular pre-images q 1 and q 2 in M and Π 1 ∩ Π 2 is a line. According to the classification in [8, Table 1], P is the image of a singularity of type A 2 0 of the mapping p. -Triple point. P ∈ Ω is a triple point if it has three regular pre-images q 1 , q 2 and q 3 and ∩ {1≤i≤3} Π i is a point. According to the classification in [8, Table 1], P is the image of a singularity of type A 3 0 of the mapping p. -Cross-cap. P ∈ Ω is a cross-cap if it has one critical pre-image q in M and q is a singularity of type cross-cap of p according to Definition 7. According to the classification in [8, Table 1], P is the image of a singularity of type S 0 of the mapping p.

regular point triple point cross-cap double point M ⊂ R 4 Ω = p(M) ⊂ R 3 p t t t 3 t 2 t 1 t 1 t 2
We use the following characterization of cross-caps in our particular setting. It is adapted from [START_REF] Mond | Classification of certain singularities and applications to differential geometry[END_REF] and a private communication with David Mond, a proof is in the appendix.

Lemma 1 ([12]

). The projection p has a singularity of type cross-cap iff the direction of projection is in the tangent plane and assuming wlog (indeed the surface can be parameterized by either (x, t), (y, t) or (z, t)) that M has a local parameterization of the form (a(z, t), b(z, t), z, t), one has ∂ zt a∂ tt b-∂ tt a∂ zt b = 0.

Transversality and genericity

For the results of Section 3, we introduce the relevant tools from singularity theory and in particular the notion of transversality.

Definition 4 ([4, Definition 2.5.1]).

Let E be a finite-dimensional vector space, the subspaces T and T are transverse if T + T = E.

The notion of transversality extends to functions via the tangent map.

Definition 5 ([4, Definition 3.7.1])

. Let E, F be finite vector spaces, V and W be submanifolds of E and F respectively, and

f ∈ C ∞ (V ; F ). -f is transverse to W at q ∈ V if either f (q) does not belong to W or f (q)
belongs to W and the image of the tangent space T q V by the tangent linear map df (q) is transverse to the tangent space

T f (q) W. -f is transverse to W if it is transverse to W at every point q of V.

Definition 6 ([4, §3.8.3]).

Let r be a non-negative integer and E, F two finitedimensional vector spaces. Let V be a submanifold of E and f ∈ C ∞ (V ; F ). Then, the map

j r f : V → J r (V, F ) q → (q, f (q), f (q), . . . , f (r) (q))
is called the r-jet of f and J r (V, F ) is called the space of jets of order r of maps from V to F .

In our setting, p is a mapping from M to R 3 . We denote by Σ 1 the submanifold of J 1 (M, R 3 ) of jets of corank 1, that is such that the linear map the jet defines from T q M to R 3 has corank 1 (with corank = min(dim(M), R 3 )-rank = 2-rank). We then denote Σ 1 (p) = (j 1 p) -1 (Σ 1 ).

Definition 7 ([6, Definition 4.5]). A point

q of M is a cross-cap of p if it is in Σ 1 (p) and j 1 p is transverse to Σ 1 at q.
We now state Thom's transversality theorem which is the main tool to determine the generic properties of projected surfaces (see Theorem 1).

Proposition 1 ([4, Theorem 3.9.4]). Let E and F be two finite-dimensional vector spaces, with U an open set in E. Let r be an integer, and let

W be a submanifold of J r (U ; F ). Then the set of maps f ∈ C ∞ (U ; F ) such that j r f is transverse to W is a dense residual subset of C ∞ (U ; F ). In other words, for generic f in C ∞ (U ; F ) the map j r f is transverse to W . In addition, in this case, (j r f ) -1 (W ) is a submanifold of U of codimension equal to codim(W ).
Finally, we show that the subset S compact of mappings that define a compact set is open, such that a residual subset of C ∞ mappings is also a residual set in the set of mappings that define implicitly compact sets.

Lemma 2. S compact is open in C ∞ (R 4 , R 2 ) equipped with the Whitney topology. Proof. If f n is a sequence that converges toward f in C ∞ (R 4 , R 2
), then according to [6, p.43], there exists a compact set K ⊂ R 4 and an integer n such that

f n (x) = f (x) for all x ∈ R 4 \ K. This implies that C ∞ (R 4 , R 2 ) \ S compact is a closed set, which concludes the proof.

Generic properties of projected surfaces

In this section, we prove Theorem 1 describing the expected geometric structure of a projected surface, it is similar to [START_REF] Demazure | Bifurcations and catastrophes: geometry of solutions to nonlinear problems[END_REF]Prop. 4.7.8] for the apparent contour of a generic surface in R 3 .

Proof (of Theorem 1)

. First, we remark that if M is a smooth compact surface, and p is a point of Ω that has one regular pre-image q by p, then it is a regular point of Ω. Indeed by the regularity of q, there exists a neighbourhood U of q in M such that all points of U are regular for the projection p. Moreover, let us show that there exists a neighbourhood V of p such that p -1 (V ) ⊂ U , then p is an embedding between p -1 (V ) and V and thus p is a regular point of Ω. By contradiction, assume that for any neighbourhood V of p, p -1 (V ) ⊂ U . Then one can construct a sequence p i ∈ Ω converging to p such that q i = p -1 (p i ) ∈ U . By compacity of M, one can assume that q i converges to q ∈ M. By continuity of p, p(q ) = p and since p has a unique pre-image, one conclude that q = q. This is in contradiction with the fact that the q i are not in U which is a neighbourhood of q.

Using the Transversality Theorem 1 and its multijet version [4, Thm 3.9.7] we prove that generically: (a) M is smooth, (b) if a point of Ω has 2 pre-images by p then it is a double point, (c) if a point of Ω has more than 2 pre-images then it is a triple point, (d) if a point p of Ω has a pre-image q and the tangent plane to M at q is vertical, then p is a cross-cap.

Let ∆ (n) (U ) denote the subset of U n consisting of n-tuples of pairwise distinct points and let J r (n) (U, F ) be the space of n-multijets of order r of maps from U to F (see [4, §3.9.6] for details). The idea is to express a geometric property as a submanifold of a jet space J r (n) (U, F ) such that the number of equations defining this submanifold coincides with its codimension. The transversality theorem then yields that generically the geometric property is satisfied on a submanifold of the original space with the same codimension. In particular when the codimension is larger than the dimension of the original space this means that the geometric property generically does not hold.

(a) Consider the jet of order 0:

j 0 (F, G) : R 4 → J 0 (R 4 , R 2 ) q → (q, F (q), G(q)).
The set W = {F (q) = G(q) = 0} is a linear submanifold of J 0 (R 4 , R 2 ) of codimension 2. The transversality theorem yields that, generically, the set

M = j 0 (F, G) -1 (W ) is a smooth surface, i.e. a 2-dimensional submanifold of R 4 . (b) Let q i = (x i , y i , z i , t i ) in R 4 .
We consider the 2-multijet defined by:

j 1 (2) (F, G) : ∆ (2) (R 4 ) → J 1 (2) (R 4 , R 2 ) (q 1 ,
q 2 ) → (q 1 , F (q 1 ), G(q 1 ), ∇F (q 1 ), ∇G(q 1 ),

q 2 , F (q 2 ), G(q 2 ), ∇F (q 2 ), ∇G(q 2 )). The set W = {x 1 = x 2 , y 1 = y 2 , z 1 = z 2 , F (q 1 ) = G(q 1 ) = F (q 2 ) = G(q 2 ) = 0} is a linear submanifold of J 1 (2) (R 4 , R 2 ) of codimension 7.
The transversality theorem yields that, generically, the set of pairs of distinct points of M that project to the same point of Ω = p(M) is a 1-dimensional submanifold of ∆ (2) (R 4 ). In addition, generically, both points q i are regular points of the projection p, since if it were not the case and q 1 were critical then this would add the two equations ∂ t F (q 1 ) = ∂ t G(q 1 ) = 0. This defines a 9-codimensional submanifold of J 1 (2) (R 4 , R 2 ) which pull back in ∆ (2) (R 4 ) of dimension 8 must be void. Similarly, adding the condition that the tangent spaces Π 1 and Π 2 coincide would add two equations to W and thus generically does not hold. (c) Consider the 3-multijet

j 0 (3) (F, G) : ∆ (3) (R 4 ) → J 0 (3) (R 4 , R 2 ) (q 1 ,
q 2 , q 3 ) → (q 1 , F (q 1 ), G(q 1 ), q 2 , F (q 2 ), G(q 2 ), q 3 , F (q 3 ), G(q 3 ))

The condition to have 3 points in M that project to the same point in Ω can be written in [START_REF] Mond | Classification of certain singularities and applications to differential geometry[END_REF], that is exactly the dimension of ∆ (3) (R 4 ). By the transversality theorem, there is thus generically a discrete set of such points. In addition, extending this jet at order 1, the condition that the intersection of the tangent planes ∩ 3 i=1 Π i is not a point or one of the points is critical for the projection would add other equations and thus this generically does not occur. Similarly, using a 4-multijet, one proves that there cannot be more than 3 distinct points projecting to the same point. The set of triple points of Ω is thus generically a discrete set. (d) Consider the jet of order 1:

J 0 (3) (R 4 , R 2 ) as {x 1 = x 2 = x 3 , y 1 = y 2 = y 3 , z 1 = z 2 = z 3 , F (q i ) = G(q i ) = 0, 1 ≤ i ≤ 3} which is a submanifold of codimension
j 1 (F, G) : R 4 → J 1 (R 4 , R 2 )
q → (q, F (q), G(q), ∇F (q), ∇G(q))

The set critical points of p can be written in J 1

(R 4 , R 2 ) as {F (q) = G(q) = ∂ t F (q) = ∂ t G(q) =
0} which is a submanifold of codimension 4, so that generically there is a discrete set of such points. To prove that these are generically cross-caps using Lemma 1, one has to use a jet of order 2 together with a local parameterization of M to see that with the additional condition

∂ zt a ∂ tt b -∂ tt a ∂ zt b = 0 one defines a submanifold of codimension 5.
The conclusion is that, generically, the singular points of Ω have at most 3 pre-images. When there is only one pre-image, it is a critical point of p and the point on Ω is a cross-cap. When there are 2 or 3 pre-images they are all regular points of p, and this gives a 1-dimensional curve of double points with a discrete set of triple points.

Computing the singularities of the projected surface

Within this section, we assume the generic properties of Theorem 1 hold. The surface Ω is thus the disjoint union of regular points, double points, triple points and cross-caps.

Systems encoding singularities

We define the systems (S-dble), (S-tple) and (S-cros) to encode the singularities of the surface Ω in higher dimensional spaces. Figure 1 illustrates the geometry of these systems.

     F (x, y, z, t1) = 0 G(x, y, z, t1) = 0 F (x, y, z, t2) = 0 G(x, y, z, t2) = 0 t1 = t2 (S-dble)          F (x, y, z, t1) = 0 G(x, y, z, t1) = 0 F (x, y, z, t2) = 0 G(x, y, z, t2) = 0 F (x, y, z, t3) = 0 G(x, y, z, t3) = 0 ti = tj f or i = j. (S-tple) F (x, y, z, t) = 0 G(x, y, z, t) = 0 ∂tF (x, y, z, t) = 0 ∂tG(x, y, z, t) = 0 (S-cros)
One remarks that the solutions of system (S-dble) come in pairs by exchanging the t 1 and t 2 coordinates. Also a solution of system (S-tple) yields three pairs of solutions of system (S-dble). We will define in Section 4.3 the additional system (S-Ball) that gathers the double points, the triple points and the cross-caps. This subsection is devoted to the proof of the following theorem. Theorem 3. A point p = (x, y, z) ∈ Ω is a 1. Double point iff it has exactly two regular pre-images (x, y, z, t 1 ) and (x, y, z, t 2 ), and the Jacobian matrix associated to (S-dble) has maximum rank at (x, y, z, t 1 , t 2 ).

Triple point iff it has three regular pre-images that give a regular solution of (S-tple). 3. Cross-cap iff it has one critical pre-image that is a regular solution of (Scros).

Regularity

We decompose the proof of Theorem 3 in several lemmas. We show that, generically, the double points are encoded by the system (S-dble) where its Jacobian has maximum rank (Lemma 3), the triple points are encoded by the regular solutions of system (S-tple) (Lemma 4) and the cross-caps are encoded by the regular solutions of system (S-cros) (Lemma 5).

Lemma 3. [Theorem 3(1)]

A point P = (x, y, z) in Ω is a double point iff it has two regular pre-images q 1 = (x, y, z, t 1 ) and q 2 = (x, y, z, t 2 ), and the Jacobian matrix associated to (S-dble) has maximum rank at q = (x, y, z, t 1 , t 2 ).

Proof. Let P be a double point of Ω with q 1 , q 2 its regular preimages by p. Let P 1 and P 2 be the tangent planes to M at q 1 and q 2 , and Π 1 , Π 2 their projections. Since q 1 , q 2 are regular points of p, P 1 , P 2 are not vertical. The Jacobian matrix J 1 associated to the system (S-dble) is

J 1 =     ∂ x F 1 ∂ y F 1 ∂ z F 1 ∂ t1 F 1 0 ∂ x G 1 ∂ y G 1 ∂ z G 1 ∂ t1 G 1 0 ∂ x F 2 ∂ y F 2 ∂ z F 2 0 ∂ t2 F 2 ∂ x G 2 ∂ y G 2 ∂ z G 2 0 ∂ t2 G 2     with F i (x, y, z, t 1 , t 2 ) = F (x, y, z, t i ) and G i (x, y, z, t 1 , t 2 ) = G(x, y, z, t i ) for i = 1, 2.
We first show that if Π 1 ∩ Π 2 is a line, then J 1 has maximum rank at q. Consider two non-null vectors u = (u x , u y , u z , u 1 , u 2 ) and v = (v x , v y , v z , v 1 , v 2 ) in Ker(J 1 (q)), then we have

∇F (q 1 ) • (u x , u y , u z , u 1 ) = 0 ∇G(q 1 ) • (u x , u y , u z , u 1 ) = 0 and ∇F (q 2 ) • (v x , v y , v z , u 2 ) = 0 ∇G(q 2 ) • (v x , v y , v z , u 2 ) = 0.
Since the tangent plane P i to M at q i is the set of vectors orthogonal to ∇F (q i ) and ∇G(q i ) (u x , u y , u z , u 1 ) ∈ P 1 and (u x , u y , u z , u 2 ) ∈ P 2 ,

which implies that (u x , u y , u z ) ∈ Π 1 ∩ Π 2 . Similarly v ∈ Ker(J 1 (q)) implies that (v x , v y , v z ) ∈ Π 1 ∩ Π 2 . Since Π 1 ∩ Π 2 is a line, there exists λ ∈ R such that λ(u x , u y , u z ) = (v x , v y , v z ).
If λ = 0 then (v x , v y , v z ) = (0, 0, 0), which implies that the vector (0, 0, 0, v 1 ) is in P 1 . This is not possible since q 1 is a regular point of p and thus P 1 is not vertical.

If λ = 0, since P 1 is not vertical, at least one of the partial derivatives ∂ t F or ∂ t G is non-null at q 1 . Without loss of generality, one can assume that ∂ t F (q 1 ) = ∂ t1 F 1 (q) = 0. Thus u, v ∈ Ker(J 1 (q)) implies

u x ∂ x F 1 (q) + u y ∂ y F 1 (q) + u z ∂ z F 1 (q) + u 1 ∂ t1 F 1 (q) = 0 v x ∂ x F 1 (q) + v y ∂ y F 1 (q) + v z ∂ z F 1 (q) + v 1 ∂ t1 F 1 (q) = 0.
Multiplying the first line by λ and subtracting the second one where (v x , v y , v z ) is substituted by λ(u x , u y , u z ) yields (λu 1 -v 1 )∂ t1 F 1 (q) = 0, thus λu 1 -v 1 = 0 and finally v 1 = λu 1 .

Using the same approach at q 2 for the non-vertical tangent plane P 2 , one concludes that v 2 = λu 2 . So u and v are colinear vectors, thus dim(Ker(J 1 (q))) = 1 and J 1 (q) has rank 4 which is maximal.

We now show the converse statement and thus assume that the Jacobian matrix is of maximum rank. By contradiction, if Π 1 ∩ Π 2 is not a line, then it is a plane Π := Π 1 = Π 2 . In this case, one can find two vectors (u x , u y , u z ) and (v x , v y , v z ) in Π that are linearly independent.

Let u = (u x , u y , u z , u 1 , u 2 ) be such that (u x , u y , u z , u i ) is the pre-image of (u x , u y , u z ) in P i . By definition of the tangent planes, one has

∇F (q 1 ) • (u x , u y , u z , u 1 ) = 0 ∇G(q 1 ) • (u x , u y , u z , u 1 ) = 0 and ∇F (q 2 ) • (v x , v y , v z , u 2 ) = 0 ∇G(q 2 ) • (v x , v y , v z , u 2 ) = 0, thus, u is in Ker(J 1 (q)). Similarly, let v = (v x , v y , v z , v 1 , v 2 ) be such that (v x , v y , v z , v i )
is the pre-image of (v x , v y , v z ) in P i , we also have that v is in Ker(J 1 (q)). Since the vectors (u x , u y , u z ) and (v x , v y , v z ) are linearly independent, the vectors u and v are also independent so dim(Ker(J 1 (q))) ≥ 2 and J 1 (q) is not of maximum rank. Π 1 ∩ Π 2 is thus necessarily a line.

Lemma 4. [Theorem 3(2)]

A point P = (x, y, z) in Ω is a triple point iff it has three regular pre-images (x, y, z, t i ), i = 1, 2, 3 and q = (x, y, z, t 1 , t 2 , t 3 ) is a regular solution of the system (S-tple).

Proof. Let P be a point in Ω with three regular pre-images q 1 , q 2 , q 3 by p. Let P i be the tangent plane to M at q i , note that P i is not vertical since q i is a regular point of p. The Jacobian matrix J 2 associated to the system (S-tple) is

J 2 =         ∂ x F 1 ∂ y F 1 ∂ z F 1 ∂ t1 F 1 0 0 ∂ x G 1 ∂ y G 1 ∂ z G 1 ∂ t1 G 1 0 0 ∂ x F 2 ∂ y F 2 ∂ z F 2 0 ∂ t2 F 2 0 ∂ x G 2 ∂ y G 2 ∂ z G 2 0 ∂ t2 G 2 0 ∂ x F 3 ∂ y F 3 ∂ z F 3 0 0 ∂ t3 F 3 ∂ x G 3 ∂ y G 3 ∂ z G 3 0 0 ∂ t3 G 3         with F i (x, y, z, t 1 , t 2 , t 3 ) = F (x, y, z, t i ) and G i (x, y, z, t 1 , t 2 , t 3 ) = G(x, y, z, t i ) for i = 1, 2, 3. If J 2 (q) is not invertible, then there exists a non-zero vector v = (v x , v y , v z , v 1 , v 2 , v 3 ) ∈ Ker(J 2 (q)). In other words, we have ∇F (q i ) • (v x , v y , v z , v i ) = ∇G(q i ) • (v x , v y , v z , v i ) = 0 and thus (v x , v y , v z , v i ) ∈ P i . This implies that (v x , v y , v z ) ∈ ∩ 3
i=1 Π i and on the other hand, since P i is not vertical, this vector is non-null. We thus have that ∩ 3 i=1 Π i is not a point. Conversely, if ∩ 3 i=1 Π i is not a point, then there exists a non-null vector

(v x , v y , v z ) ∈ ∩ 3 i=1 Π i . Let (v x , v y , v z , v i ) ∈ P i be the pre-image of (v x , v y , v z ), we then have ∇F (q i ) • (v x , v y , v z , v i ) = ∇G(q i ) • (v x , v y , v z , v i ) = 0. In other words, J 2 (q) • (v x , v y , v z , v 1 , v 2 , v 3 ) =
0 and thus J 2 (q) is not invertible.

Lemma 5. [Theorem 3(3)] A point P = (x, y, z) in Ω is a cross-cap iff it has one critical pre-image that is a regular solution of (S-cros).

Proof. First note that for a solution q of the system (S-cros), q is in M and ∂ t F (q) = ∂ t G(q) = 0, thus the tangent plane P to M at q is vertical which is the first condition for a cross-cap in Lemma 1.

Without loss of generality, one can assume the surface parameterized by the variables z and t. Indeed, ∇F (q) and ∇G(q) are independant so that there exists a 2×2 minor with non-null determinant. If we assume det

∂ x F (q) ∂ y F (q) ∂ x G(q) ∂ y G(q) = 0
then, by the implicit function theorem, M is locally the image of a mapping (z, t) → (a(z, t), b(z, t), z, t), with a and b two smooth functions. In other words, M is the zero locus of the functions

F (x, y, z, t) = -x + a(z, t) G(x, y, z, t) = -y + b(z, t).
The Jacobian matrix of the system (S-cros) using the functions F and G is then

J3 =     -1 0 ∂ z (a) ∂ t (a) 0 -1 ∂ z (b) ∂ t (b) 0 0 ∂ zt (a) ∂ tt (a) 0 0 ∂ zt (b) ∂ tt (b)    
and its determinant reads as det( J3

) = ∂ zt (a)∂ tt (b) -∂ tt (a)∂ zt (b)
, which is precisely the quantity for the second condition of a cross-cap in Lemma 1. So we have just proved that P is a cross-cap iff det( J3 ) = 0. It remains to prove that det( J3 ) = 0 iff det(J 3 ) = 0 where J 3 is the Jacobian matrix associated to the system (S-cros):

J 3 =     ∂ x F ∂ y F ∂ z F 0 ∂ x G ∂ y G ∂ z G 0 ∂ xt F ∂ yt F ∂ zt F ∂ tt F ∂ xt G ∂ yt G ∂ zt G ∂ tt G     .
We apply Hadamard's Lemma [4, Lemma 4.2.1] twice, first to F (a+X, b+Y, z, t) with respect the variable X:

F (a + X, b + Y, z, t) -F (a, b + Y, z, t) = Xg 1 (X, b + Y, z, t) (1)
with

g 1 (0, b + Y, z, t) = ∂ x F (a, b + Y, z, t) (2)
and then to F (a, b + Y, z, t) with respect to the variable Y :

F (a, b + Y, z, t) -F (a, b, z, t) = Y g 2 (Y, z, t) with g 2 (0, z, t) = ∂ y F (a, b, z, t). ( 3
)
By definition of the parametrization (z, t) → (a(z, t), b(z, t), z, t), for any point on the surface M sufficiently close to q, F (a(z, t), b(z, t), z, t) = 0, thus equality (1) becomes

F (a + X, b + Y, z, t) = Xg 1 (X, b + Y, z, t) + Y g 2 (Y, z, t) (4)
Now we set:

X = x -a(z, t) Y = y -b(z, t).
Substituting X and Y in the relations ( 4), ( 2) and (3) yields

F (x, y, z, t) = -F (x, y, z, t)g 1 (x + a, y, z, t) -G(x, y, z, t)g 2 (b + y, z, t). ( 5
)
In the same way, applying Hadamard's Lemma to G(a + X, b + Y, z, t), there exist two smooth functions h 1 and h 2 such that

G(x, y, z, t) = -F (x, y, z, t)h 1 (x + a, y, z, t) -G(x, y, z, t)h 2 (b + y, z, t) (6) with h 1 (0, y, z, t) = ∂ x G(a, y, z, t) and h 2 (0, z, t) = ∂ y G(a, b, z, t).
We rewrite the relations ( 5) and ( 6) as

F G = - g 1 g 2 h 1 h 2 A F G = A F G . Note that at the point q, A(q) = - ∂ x F (q) ∂ y F (q) ∂ x G(q) ∂ y G(q)
and by our assumption det A(q) = 0.

Differentiating with respect to t yields

∂ t F ∂ t G = ∂ t A F G + A ∂ t F ∂ t G .
We can thus rewrite the system for cross-caps as

F G ∂ t F ∂ t G T F = A 0 ∂ t A A N F G ∂ t F ∂ t G T F . (7)
The Jacobian determinants J 3 = det(Jac(F)) and J3 = det(Jac( F)). The partial derivative of equation ( 7) with respect to any of the variables yields

∂F = ∂(N × F) = ∂N × F + N × ∂ F
, and since at the point q, F(q) = 0, this simplifies to ∂F(q) = N (q) × ∂ F(q). At the point q, we thus have the equation J 3 (q) = N (q) × J3 (q), and since det N (q) = det A(q) 2 = 0 we conclude that det J 3 (q) = 0 ⇔ det J3 (q) = 0. (8)

Ball system

In this section, we show that the system (S-Ball) represents the solutions of (Sdble), (S-tple) and (S-cros) as regular solutions of a single system of equations via a change of variables. We call this system the Ball system as in [START_REF] Imbach | Numeric and certified isolation of the singularities of the projection of a smooth space curve[END_REF] where the same approach was used for the projection of a space curve in the plane.

Lemma 6. The projections in R 3 of the solutions of the Ball system for r ≥ 0 are the projections of the solutions of systems (S-dble), (S-tple) and (S-cros).

Proof. Let (x, y, z, c, r) be a solution of the Ball system. If r = 0, the Ball system is exactly the system (S-cros). If r > 0, defining t 1 = c -√ r, t 2 = c + √ r, one can transform the Ball system into the system (S-dble) by multiplying the last two lines by √ r and adding or subtracting the two first lines by the last two ones. Finally by construction, the projection of the solutions of (S-tple) is included in the projection of the solutions of (S-dble), and thus in the projection of the solutions of the Ball system. Lemma 7. Let P = (x, y, z) be a point in Ω.

1. P is a double point iff it has two regular pre-images (x, y, z, t 1 ) and (x, y, z, t 2 )

with t 1 = t 2 such that (x, y, z, t1+t2 2 , ( t1-t2 2 ) 2 ) is a regular solution of (S-Ball). 2. If P is a triple point, then it has three pre-images that give three regular solutions of (S-Ball). 3. If P is a cross-cap, then it has one critical pre-image (x, y, z, t) such that (x, y, z, t, 0) is a regular solution of (S-Ball).

To prove Lemma 7, we first note that S.F, S.G, D.F and D.G are smooth functions. The following lemma is a variation of [START_REF] Imbach | Numeric and certified isolation of the singularities of the projection of a smooth space curve[END_REF]Lemma 6] to the case of functions of R 4 that we state without proof. Proof (Proof of Lemma 7.). For the case r > 0, according to Lemma 8, the Jacobian of (S-Ball) is

J (c,r>0) =     S.∂ x F S.∂ y F S.∂ z F S.∂ t F D.∂tF 2 S.∂ x G S.∂ y G S.∂ z G S.∂ t G D.∂tG 2 D.∂ x F D.∂ y F D.∂ z F D.∂ t F S.∂tF -D.F 2r D.∂ x G D.∂ y G D.∂ z G D.∂ t G S.∂tG-D.G 2r     .
Let q = (x, y, z, c, r) be a solution of the Ball system with r > 0, J (c,r>0) can be simplified using the fact that D.F (q) = D.G(q) = 0. Denote q 1 = (x, y, z, c+ √ r)

and q 2 = (x, y, z, c -√ r) the two points of M solutions of (S-dble) according to Lemma 6. Applying to J (c,r>0) successively the following transformations on its lines and columns:

3 ←- √ r × 3 , 4 ←- √ r × 4 , c 5 ←-(2 √ r)c 5 , 1 ←- 1 + 3 , 3 ←-1 -3 , 2 ←-2 + 4 , 4 ←-2 -4 , one has: det J (c,r>0) = 0 ⇐⇒ det     ∂ x F (q 1 ) ∂ y F (q 1 ) ∂ z F (q 1 ) ∂ t F (q 1 ) ∂ t F (q 1 ) ∂ x G(q 1 ) ∂ y G(q 1 ) ∂ z G(q 1 ) ∂ t G(q 1 ) ∂ t G(q 1 ) ∂ x F (q 2 ) ∂ y F (q 2 ) ∂ z F (q 2 ) ∂ t F (q 2 ) -∂ t F (q 2 ) ∂ x G(q 2 ) ∂ y G(q 2 ) ∂ z G(q 2 ) ∂ t G(q 2 ) -∂ t G(q 2 )     = 0 By changing again c 4 ←-1 2 (c 4 + c 5 ) and c 5 ←-1 2 (c 4 -c 5 ), we get det J (c,r>0) = 0 ⇐⇒ det     ∂ x F (q 1 ) ∂ y F (q 1 ) ∂ z F (q 1 ) ∂ t F (q 1 ) 0 ∂ x G(q 1 ) ∂ y G(q 1 ) ∂ z G(q 1 ) ∂ t G(q 1 ) 0 ∂ x F (q 2 ) ∂ y F (q 2 ) ∂ z F (q 2 ) 0 ∂ t F (q 2 ) ∂ x G(q 2 ) ∂ y G(q 2 ) ∂ z G(q 2 ) 0 ∂ t G(q 2 )     = 0
The matrix on the right hand side is exactly that of the Jacobian of the system (S-dble), thus the lemma reduces to Lemma 3. In particular, this implies that both for double points and for triple points the solutions of the Ball system are regular.

For the case r = 0, the Ball system (S-Ball) coincides with the system (Scros). In particular, according to Lemma 5, if P is cross-cap, the Jacobian of Equations (S-cros) is non-zero, which implies that the Jacobian matrix of the Ball system (S-Ball) is full rank. This implies that above cross-cap, the solution of the Ball system is regular.

Algorithm

We developed a solver optimized for multivariate high degree polynomials called voxelize and available with GPL license ( [START_REF] Moroz | Voxelize[END_REF]). It is based on a classical bisection approach with an interval exclusion test that excludes the boxes that don't satisfy the input equations and inequalities ([15, Chapter 5] and references therein). For storing the set of boxes created during the subdivision, we use the Compressed Sparse Fiber data structure [START_REF] Smith | Tensor-matrix products with a compressed sparse tensor[END_REF][START_REF] Chou | Format abstraction for sparse tensor algebra compilers[END_REF], described in the literature as a generalization of the Compressed Sparse Row format. The main advantage of this data structure is that it allows us to efficiently evaluate a polynomial on a set of boxes appearing during the subdivision algorithm. More precisely, given a set S of K boxes in R n arranged as a cube with K = k n , evaluating a polynomial of degree d on S can be done in

O(d n k + • • • + dk n ) arithmetic operations. If k > d, this leads to O(ndK) arithmetic operations.

Example

Whitney Umbrella

Our first example is the Whitney Umbrella. Its parametric equations are: x(u, v) = u, y(u, v) = v 2 and z(u, v) = uv. Letting F (x, y, z, t) = y -t 2 and G(x, y, z, t) = z -xt, the Whitney Umbrella is exactly the projection in R 3 of the surface defined by F = G = 0. The corresponding Ball system is :

     S.F = y -c 2 -r = 0 S.G = z -xc = 0 D.F = -2c = 0 D.G = -x = 0
Thus, substituting c by 0, we deduce that the set of singularities of the Whitney Umbrella is defined by x = 0, z = 0 and y = r ≥ 0. Note that most state-of-the-art approaches start by computing the implicit equation of the Whitney Umbrella: P (x, y, z) = x 2 y -z 2 = 0, and then compute the singularities of this map as P = ∂ x P = ∂ y P = ∂ z P = 0. Unfortunately, the solution to this system is x = 0 and z = 0, which adds a handle that is not a singularity of the original surface. This is a known artifact that comes from the Zariski closure of the original surface. Our method has the advantage of returning the exact set of singularities of the Whitney Umbrella, without the spurious handle.

Large polynomials

Another advantage of our approach is that it is based on numerical methods, and as such, it can compute the singularities of polynomial maps of high degrees. For example, the polynomials in Equations ( 9) are generated randomly with degree 7. Computing SF, SG, DF, DG can be done quickly with a computer algebra system. Then, using our subdivision solver voxelize, we enclosed the solutions of the Ball system within the input box x = [-0.35, 0.35], y = [-0.35, 0.35], z = [0.4, 1.1], c = [-5, 5], r = [0, 5]. Our result is displayed on Figure 2, the red curve is the projection in R 3 of the boxes of R 5 enclosing the Ball system, each box being of size a factor 2 -11 of the size of the input box. The surface F = G = 0 is also enclosed by voxelize in boxes in R 4 , we then use a generalization to 4D of the SurfaceNet approach [START_REF] Gibson | Constrained elastic surface nets: Generating smooth surfaces from binary segmented data[END_REF][START_REF] De Bruin | Improving triangle mesh quality with surfacenets[END_REF] to compute a mesh that is eventually projected in R 3 and displayed on the left of Figure 2. On a quadcore Intel CPU i7-8650U, voxelize running time was 11 seconds to enclose the Ball system and 8.5 seconds to enclose the surface and compute its meshing.

Conclusion

As shown in the examples, our approach handles computation of singularities not handled by other state-of-the-art methods. Moreover, even though our approach cannot handle the computation of the singularities associated to any mapping, we showed that our approach works for almost all mappings.

With the systems we describe in Section 4.1, we could also compute the triple points and the cross-cap singularities. Note that in order to make this computation reliable, we need additional computation, not covered here, to ensure that we don't miss triple-points near cross-caps. nication, this proof of the characterization of cusps.

Let q ∈ M be a cross-cap singularity of the projection p : M → R 3 . First, the condition q ∈ Σ 1 (p) means that dp(q) has corank 1. Since rank(p) = 2 -corank(p) = 1, the condition is also equivalent to dp(q) has rank 1. In other words, the 2-dimensional tangent plane to M at q projects to a line, that is the direction of projection is in the tangent plane. Thus, the condition q ∈ Σ 1 (p) of Definition 7 is equivalent to the first condition of Lemma 1: the direction of projection is in the tangent plane.

We now assume that the surface M is locally parameterized in a neighborhood of q by (z, t) → (a(z, t), b(z, t), z, t), so that p(z, t) = (a(z, t), b(z, t), z). The space J 1 (M, R 3 ) is thus locally equal to U × R 3 × L(R 2 , R 3 ) where U is a subset of R 2 and L stands for the space of linear mappings. The 1-jet of a mapping (f1(z, t), f2(z, t), f3(z, t)) : M → R 3 is (z, t), (f1(z, t), f2(z, t), f3(z, t)), f1z f1t f2z f2t f3z f3t . Σ 1 is the subset of J 1 (M, R 3 ) such that the matrix f1z f1t f2z f2t f3z f3t has corank 1, that is has rank 1. Without loss of generality, if we assume (f3z, f3t) = (0, 0), Σ 1 is thus implicitly defined by the two equations: f1z f1t f3z f3t = 0 and f2z f2t f3z f3t = 0. One thus has Σ 1 = Φ -1 (0) with Φ : J 1 (M, R 3 ) → R 2 (z, t), (f1(z, t), f2(z, t), f3(z, t)), f1z f1t f2z f2t f3z f3t

→ f1zf3t -f1tf3z f2zf3t -f2tf3z
According to [6, Lemma 4.3], j 1 p is transverse to Σ 1 at q iff Φ • j 1 p is a submersion at q.

On the other hand, Φ • j 1 p = Φ (z, t), (a(z, t), b(z, t), z), az at bz bt 1 0

= -(at, bt). This mapping is a submersion iff its Jacobian azt att bzt btt is full rank, that is aztbtt-attbzt = 0 which is exactly the second condition of Lemma 1.

Fig. 1 :Definition 3 .

 13 Fig. 1: Types of singularities of Ω = p(M) with their pre-images on M

Lemma 8 .

 8 If A is a real smooth function, then S.A and D.A are real smooth functions. Moreover, the derivatives of S.A with respect to x, y, z, c, r are respectively S.∂ x A, S.∂ y A, S.∂ z A, S.∂ t A, 1 2 D.∂ t A. The derivatives of D.A with respect to x, y, z, c, r are respectively D.∂ x A, D.∂ y A, D.∂ z A, D.∂ t A and 1 2r (S.∂ t A-D.A) if r > 0 and 1 6 ∂ tt A if r = 0.

Acknowledgment:

We thanks David Mond for providing to us, via a private commu-

Finally, it is also possible to check the assumptions satisfied generically in Theorem 1 using a semi-algorithm that terminates if and only if the required conditions are satisfied, such an approach is exemplified in a close setting in [START_REF] Imbach | A certified numerical algorithm for the topology of resultant and discriminant curves[END_REF].