Finitely many directions detecting ambient order uniformly

For a fixed total degree bound, finitely many fixed affine directions detect the ambient order of every polynomial at every center. The directions may be chosen in any box with infinite sides. The ambient order is the minimum of the orders of the line restrictions.

Keeping one distinguished coordinate free gives a stronger geometric application: finitely many transverse planes detect ambient order uniformly. Thus constancy of order in those plane families implies constancy of full ambient order, rather than merely an inequality or equality at one chosen center. Infinite orders are retained for zero polynomials. Zero base directions and zero-dimensional bases are included.

References

S. McCallum, An improved projection operation for cylindrical algebraic decomposition, Springer (1998), Sections 2–3 (ambient order and transverse restrictions).

theorem TauCeti.exists_finset_orderAt_eq_iInf_trailingDegree {σ : Type u_1} {K : Type u_2} [Field K] [Finite σ] (D : ℕ) (s : σ → Set K) (hs : ∀ (i : σ), (s i).Infinite) : ∃ (T : Finset (σ → K)), ↑T ⊆ Set.univ.pi s ∧ ∀ (p : MvPolynomial σ K), p.totalDegree ≤ D → ∀ (a : σ → K), p.orderAt a = ⨅ (v : ↥T), ((MvPolynomial.aeval fun (i : σ) => Polynomial.C (a i) + Polynomial.C (↑v i) * Polynomial.X) p).trailingDegree

With a fixed degree bound, finitely many directions in any box with infinite sides detect ambient order at every center, for every polynomial within that bound.

theorem TauCeti.exists_finset_orderAt_eq_iInf_transverse {K : Type u_2} [Field K] (n D : ℕ) (s : Fin n → Set K) (hs : ∀ (i : Fin n), (s i).Infinite) : ∃ (T : Finset (Fin n → K)), ↑T ⊆ Set.univ.pi s ∧ ∀ (p : MvPolynomial (Fin (n + 1)) K), p.totalDegree ≤ D → ∀ (a : Fin (n + 1) → K), p.orderAt a = ⨅ (v : ↥T), ((MvPolynomial.aeval (Fin.cons (MvPolynomial.C (a 0) + MvPolynomial.X 1) fun (i : Fin n) => MvPolynomial.C (a i.succ) + MvPolynomial.C (↑v i) * MvPolynomial.X 0)) p).orderAt 0

Finitely many fixed base directions detect ambient order on transverse planes at all centers, uniformly for polynomials of bounded total degree. The plane coordinates are the base-line parameter and the distinguished root coordinate, respectively.