Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

On Projective Delineability

Lucas Michel, Jasper Nalbach, Pierre Mathonet, Naïm Zénaïdi, Christopher W. Brown, Erika Ábrahám, James H. Davenport, Matthew England

TL;DR

The paper introduces projective delineability as a projective-geometry–based surrogate for classical delineability in cylindrical algebraic decomposition. By leveraging the real projective line $\\mathbb{RP}^1$, homogenization, and linear-transform pullbacks $H^d$, $\\iota_A^{*d}$, and $A^{*d}$, it formalizes projective roots and proves local and global results that mirror McCallum’s delineability theory, enabling omission of leading coefficients in single-cell CAD constructions. The local result uses a geometric trick to avoid roots at infinity, after which standard delineability applies and transfers back to the projective setting; the global result shows that on simply connected bases the projective delineability data form a trivial cover, yielding global root functions. Together, these findings provide a framework for computational savings in CAD, with potential practical impact for SMT-based real arithmetic decision procedures, and extend cleanly to multivariate polynomials. The work thus offers a principled path to reduce projection data while preserving correct regionwise sign-invariance in CAD computations.

Abstract

We consider cylindrical algebraic decomposition (CAD) and the key concept of delineability which underpins CAD theory. We introduce the novel concept of projective delineability which is easier to guarantee computationally. We prove results about this which can allow reduced CAD computations.

On Projective Delineability

TL;DR

The paper introduces projective delineability as a projective-geometry–based surrogate for classical delineability in cylindrical algebraic decomposition. By leveraging the real projective line , homogenization, and linear-transform pullbacks , , and , it formalizes projective roots and proves local and global results that mirror McCallum’s delineability theory, enabling omission of leading coefficients in single-cell CAD constructions. The local result uses a geometric trick to avoid roots at infinity, after which standard delineability applies and transfers back to the projective setting; the global result shows that on simply connected bases the projective delineability data form a trivial cover, yielding global root functions. Together, these findings provide a framework for computational savings in CAD, with potential practical impact for SMT-based real arithmetic decision procedures, and extend cleanly to multivariate polynomials. The work thus offers a principled path to reduce projection data while preserving correct regionwise sign-invariance in CAD computations.

Abstract

We consider cylindrical algebraic decomposition (CAD) and the key concept of delineability which underpins CAD theory. We introduce the novel concept of projective delineability which is easier to guarantee computationally. We prove results about this which can allow reduced CAD computations.

Paper Structure

This paper contains 10 sections, 12 theorems, 27 equations, 3 figures.

Table of Contents

  1. Introduction
  2. Delineability and Leading Coefficients
  3. Preliminaries
  4. The projective line
  5. Binary forms, homogenizations and pull-backs
  6. Projective roots, resultants and discriminants
  7. Extensions to multivariate polynomials
  8. Projective delineability
  9. Local Result
  10. Global result and coverings

Key Result

Lemma 1

For every $d\in\mathbb{N}$ and $A,B\in GL(2,\mathbb{R})$, we have $\iota_A^{*d}\circ H^d_B=\iota^{*d}\circ R_{B^{-1}A}\circ H^d$. In particular, we have $\iota_A^{*d}=\iota^{*d}\circ R_A$, and $H^d_A=R_{A^{-1}}\circ H^d.$

Figures (3)

  • Figure 1: The sets of roots of $P$ (red) and $Q$ (green) seen in $\mathbb{R}^2$ (left) and in $\mathbb{R} \times \mathbb{RP}^1$ (right)
  • Figure 2: A visualization of $Z_{\mathbb{RP}^1}(P,\mathbb{R})$ with the blue line $x_2 = 1$ (top) and $Z_{\mathbb{RP}^1}(A^{*2}P,\mathbb{R})$ with the black line $x_2 = -1$ (bottom).
  • Figure 3: $S$ (blue), $Z_{\mathbb{R}}(P, \mathbb{R}^2)$ (orange) and $Z_{\mathbb{R}}(P,S)$ (red)

Theorems & Definitions (44)

  • Definition 1: collins1975McCallum1988
  • Example 1
  • Definition 2
  • Definition 3
  • Remark 1
  • Definition 4
  • Remark 2
  • Lemma 1
  • proof
  • Definition 5
  • ...and 34 more