Semialgebraic descriptions of shared roots

The shared roots of a finite polynomial family are the union of the distinct roots of its nonzero specializations. Their number, and their number below a polynomial threshold, have finite polynomial sign descriptions. In cylinder coordinates this gives the graph of each ordered shared root and every complementary sector, including the two unbounded sectors.

At each parameter, only the active (nonzero) specializations enter the product. Stratifying by this active subfamily reduces the descriptions to the uniform single-polynomial root formulas. No closure under projection, constancy of degrees, or continuity of roots is needed. Repeated roots and roots shared by several members are counted once. A nullified member is omitted: its entire zero set is not part of the finite shared root set. When all members are nullified, or the family is empty, the shared root set is empty and sector zero is the whole fiber.

References

S. Basu, R. Pollack, and M.-F. Roy, Algorithms in Real Algebraic Geometry, second edition, Chapters 10 and 11 (uniform sign descriptions and the roots of an active polynomial family).

theorem Finset.isSemialgebraic_setOf_mem_biUnion_roots_map_eval {σ : Type u_1} {R : Type u_2} [CommRing R] [IsDomain R] [LinearOrder R] (F : Finset (Polynomial (MvPolynomial σ R))) (T : MvPolynomial σ R) : TauCeti.IsSemialgebraic {x : σ → R | (MvPolynomial.eval x) T ∈ F.biUnion fun (P : Polynomial (MvPolynomial σ R)) => (Polynomial.map (MvPolynomial.eval x) P).roots.toFinset}

Membership in the shared distinct root set at a polynomial threshold is semialgebraic. Zero specializations are omitted, rather than contributing their entire zero set.

theorem Finset.isSemialgebraic_setOf_card_biUnion_roots_map_eval {σ : Type u_1} {R : Type u_2} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R] (F : Finset (Polynomial (MvPolynomial σ R))) (k : ℕ) : TauCeti.IsSemialgebraic {x : σ → R | (F.biUnion fun (P : Polynomial (MvPolynomial σ R)) => (Polynomial.map (MvPolynomial.eval x) P).roots.toFinset).card = k}

The number of shared distinct roots is semialgebraic in the parameters, even when members are nullified or their degrees drop. An empty active subfamily has count zero.

theorem Finset.isSemialgebraic_setOf_card_biUnion_roots_map_eval_lt {σ : Type u_1} {R : Type u_2} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R] (F : Finset (Polynomial (MvPolynomial σ R))) (T : MvPolynomial σ R) (k : ℕ) : TauCeti.IsSemialgebraic {x : σ → R | {r ∈ F.biUnion fun (P : Polynomial (MvPolynomial σ R)) => (Polynomial.map (MvPolynomial.eval x) P).roots.toFinset | r < (MvPolynomial.eval x) T}.card = k}

The number of shared distinct roots strictly below a polynomial threshold is semialgebraic. The strict inequality includes the case where the threshold is itself a shared root.

theorem Finset.isSemialgebraic_setOf_mem_biUnion_roots_card_lt {R : Type u_2} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R] {n : ℕ} (F : Finset (Polynomial (MvPolynomial (Fin n) R))) (i : ℕ) : TauCeti.IsSemialgebraic {y : Fin (n + 1) → R | (y 0 ∈ F.biUnion fun (P : Polynomial (MvPolynomial (Fin n) R)) => (Polynomial.map (MvPolynomial.eval (Fin.tail y)) P).roots.toFinset) ∧ {r ∈ F.biUnion fun (P : Polynomial (MvPolynomial (Fin n) R)) => (Polynomial.map (MvPolynomial.eval (Fin.tail y)) P).roots.toFinset | r < y 0}.card = i}

The graph of the ith ordered shared distinct root, counted from zero, is semialgebraic in cylinder coordinates. Where fewer than i + 1 shared roots exist the fiber is empty.

theorem Finset.isSemialgebraic_setOf_notMem_biUnion_roots_card_lt {R : Type u_2} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R] {n : ℕ} (F : Finset (Polynomial (MvPolynomial (Fin n) R))) (j : ℕ) : TauCeti.IsSemialgebraic {y : Fin (n + 1) → R | (y 0 ∉ F.biUnion fun (P : Polynomial (MvPolynomial (Fin n) R)) => (Polynomial.map (MvPolynomial.eval (Fin.tail y)) P).roots.toFinset) ∧ {r ∈ F.biUnion fun (P : Polynomial (MvPolynomial (Fin n) R)) => (Polynomial.map (MvPolynomial.eval (Fin.tail y)) P).roots.toFinset | r < y 0}.card = j}

The locus of the jth shared-root sector, counted from below, is semialgebraic. Sector zero is the whole fiber if no active member has a root.