Simultaneous delineating refinement over a point

The roots of the delineating sets of a finite polynomial family cut the line over a base point into one common stack. Every input has constant ambient order on each cell, even when some or all inputs are nullified over that point. The section list contains exactly those distinct roots; its length is bounded by the sum of the degrees of the delineating polynomials.

Over the reals, this is a semialgebraic stack of analytic submanifolds: its sections have dimension zero and its sectors have dimension one. Every input is also sign-invariant on each cell. This supplies the simultaneous local refinement needed when lifting a polynomial family over a zero-dimensional base cell. The cell version accepts any preconnected zero-dimensional analytic submanifold: its chart condition forces it to be a singleton. The empty family and zero polynomials are allowed.

References

• S. McCallum, An improved projection operation for cylindrical algebraic decomposition, Springer (1998), 242–268.
• C. W. Brown, The McCallum projection, lifting, and order-invariance, technical report USNA-CS-TR-2005-02, U.S. Naval Academy (2005).

theorem Finset.exists_strictMono_orderAt_eq_of_mem_stackCells {R : Type u_1} [CommRing R] [IsDomain R] [LinearOrder R] [IsAddTorsionFree R] {n : ℕ} (F : Finset (MvPolynomial (Fin (n + 1)) R)) (α : Fin n → R) : ∃ (k : ℕ) (c : Fin k → R), StrictMono c ∧ (∀ (t : R), t ∈ Set.range c ↔ ∃ f ∈ F, ∃ q ∈ f.delineatingSet α, q.IsRoot t) ∧ k ≤ ∑ f ∈ F, ∑ q ∈ f.delineatingSet α, q.natDegree ∧ ∀ f ∈ F, ∀ E ∈ TauCeti.stackCells {α} fun (i : Fin k) (x : ↑{α}) => c i, ∀ y ∈ E, ∀ y' ∈ E, f.orderAt y = f.orderAt y'

The distinct roots of all delineating sets of a finite family give a common, strictly ordered stack over a point, on whose cells every input has constant ambient order. The number of sections is bounded by the sum of the delineating polynomials' degrees.

theorem Finset.exists_isSemialgebraicStack_orderAt_eq {n : ℕ} (F : Finset (MvPolynomial (Fin (n + 1)) ℝ)) (α : Fin n → ℝ) : ∃ (k : ℕ) (c : Fin k → ℝ), (TauCeti.IsSemialgebraicStack {α} fun (i : Fin k) (x : ↑{α}) => c i) ∧ (∀ (t : ℝ), t ∈ Set.range c ↔ ∃ f ∈ F, ∃ q ∈ f.delineatingSet α, q.IsRoot t) ∧ k ≤ ∑ f ∈ F, ∑ q ∈ f.delineatingSet α, q.natDegree ∧ ∀ E ∈ TauCeti.stackCells {α} fun (i : Fin k) (x : ↑{α}) => c i, (∃ d ≤ 1, TauCeti.IsAnalyticSubmanifold d E) ∧ ∀ f ∈ F, (∀ y ∈ E, ∀ y' ∈ E, f.orderAt y = f.orderAt y') ∧ TauCeti.SignInvariant (fun (y : Fin (n + 1) → ℝ) => (MvPolynomial.eval y) f) E

Simultaneous refinement over a real base point gives a semialgebraic stack with a bounded number of sections. Every cell is an analytic submanifold of dimension zero or one, and every input polynomial has constant ambient order and sign on it. This includes nullified inputs.

theorem Finset.exists_isSemialgebraicStack_orderAt_eq_of_isAnalyticSubmanifold_zero {n : ℕ} (F : Finset (MvPolynomial (Fin (n + 1)) ℝ)) {S : Set (Fin n → ℝ)} (hS : TauCeti.IsAnalyticSubmanifold 0 S) (hconn : IsPreconnected S) : ∃ (k : ℕ) (c : Fin k → ℝ), (TauCeti.IsSemialgebraicStack S fun (i : Fin k) (x : ↑S) => c i) ∧ (∀ α ∈ S, ∀ (t : ℝ), t ∈ Set.range c ↔ ∃ f ∈ F, ∃ q ∈ f.delineatingSet α, q.IsRoot t) ∧ (∀ α ∈ S, k ≤ ∑ f ∈ F, ∑ q ∈ f.delineatingSet α, q.natDegree) ∧ ∀ E ∈ TauCeti.stackCells S fun (i : Fin k) (x : ↑S) => c i, (∃ d ≤ 1, TauCeti.IsAnalyticSubmanifold d E) ∧ ∀ f ∈ F, (∀ y ∈ E, ∀ y' ∈ E, f.orderAt y = f.orderAt y') ∧ TauCeti.SignInvariant (fun (y : Fin (n + 1) → ℝ) => (MvPolynomial.eval y) f) E

Simultaneous delineating refinement over a preconnected zero-dimensional analytic cell. Every input has constant ambient order and sign on every part, including nullified inputs. The resulting parts are analytic submanifolds of dimension zero or one, and the number of sections is bounded by the degrees of the mixed-derivative specializations at any base point. No singleton representation of the base cell is required.