Delineations of families of real polynomials

Let P k x, for k in an index type ι, be real polynomials depending on a parameter x in a base X. A delineation of P is a common stack for the whole family: finitely many continuous functions θ₀ < θ₁ < ⋯ < θₘ₋₁ on X such that

• each member is either the zero polynomial at every point of the base or at none, and has the same degree at every point;
• at every point, the roots of every nonzero member are among the values θᵢ x, every θᵢ x is a root of some member, and the multiplicity of θᵢ x as a root of P k x does not depend on x;
• every member is sign-invariant on each section and each sector of the stack.

This is the conclusion of Collins' delineability theorem, the step that lifts a cylindrical algebraic decomposition by one dimension.

Over a nonempty base the ordered list of root functions of a delineation is the increasing enumeration of the real roots of the nonzero members, so a delineation is unique. Delineations restrict along continuous maps of bases.

The main theorem TauCeti.nonempty_delineation constructs a delineation over a preconnected base from invariant algebraic data: if the coefficients of every member are continuous, every member is nullified everywhere or nowhere, and the degree of every member, its number of distinct complex roots and the degree of the gcd of every pair of distinct members are constant on the base, then the family has a delineation. Its root functions are the common ordered real roots given by the family matching lemma Polynomial.exists_continuous_ordered_common_roots_of_preconnectedSpace.

When the derivative of every member is zero or a member, Thom's lemma shows that two points of one fiber at which all members have the same signs lie in the same section or sector. So the cells of the stack are cut out by sign conditions on the members.

For a family obtained from polynomials f in n + 1 variables by singling out the first one with MvPolynomial.finSuccEquiv, every f is sign-invariant on each cell of the stack in ℝ^(n + 1), the cells being the images of the sections and sectors under TauCeti.cylinder.

Main declarations

• TauCeti.Delineation: a common stack of the roots of a family of real polynomials.
• TauCeti.Delineation.range_root: the root functions enumerate the real roots of the nonzero members.
• TauCeti.Delineation.isRoot_iff: the roots of a nonzero member are the sections in which it has positive multiplicity.
• TauCeti.Delineation.instSubsingleton: over a nonempty base a family has at most one delineation.
• TauCeti.Delineation.comp: restriction of a delineation along a continuous map of bases.
• TauCeti.nonempty_delineation: existence of a delineation over a preconnected base from constant degrees, numbers of distinct complex roots and pairwise gcd degrees.
• TauCeti.exists_delineation_of_isRoot_iff: an ordered continuous enumeration of the real roots of a single nowhere-zero family, with constant multiplicities, is a delineation.
• TauCeti.exists_delineation_ball_of_isRoot_iff: the local version on a ball in a real normed space, for families that are nonzero, of constant degree and with continuous coefficients near the center.
• TauCeti.Delineation.root_notMem_uIcc_of_sign_eval_eq, TauCeti.Delineation.mk_mem_sectionSet_iff_of_sign_eval_eq, TauCeti.Delineation.mk_mem_sectorSet_iff_of_sign_eval_eq: when the derivative of every member is zero or a member, points of one fiber with the same signs are not separated by the stack.
• TauCeti.Delineation.signInvariant_eval₂_of_mem_stackCells: the polynomials in n + 1 variables behind a family are sign-invariant on every ambient cell of a delineation.

References

S. Basu, R. Pollack, and M.-F. Roy, Algorithms in Real Algebraic Geometry, second edition, Section 5.1 (Theorem 5.16).

structure TauCeti.Delineation {X : Type u_1} {ι : Type u_3} [TopologicalSpace X] (P : ι → X → Polynomial ℝ) : Type (max u_1 u_3)

A delineation of a family P k x of real polynomials over a base X is a common stack of their roots: continuous functions root 0 < ⋯ < root (count - 1) on X such that each member is zero everywhere or nowhere and has constant degree, the roots of each nonzero member are among the root i x, each root i is a root of some member, the multiplicity of root i x as a root of P k x is a constant multiplicity k i, and each member is sign-invariant on every section and every sector of the stack.

• count : ℕ

  The number of sections of the stack.

• root : Fin self.count → X → ℝ

  The root functions, listed in increasing order.

• continuous_root (i : Fin self.count) : Continuous (self.root i)

  Each root function is continuous.

• strictMono_root (x : X) : StrictMono fun (i : Fin self.count) => self.root i x

  At each point the root functions are strictly increasing in their index.

• multiplicity : ι → Fin self.count → ℕ

  The multiplicity of the i-th root function as a root of the k-th member.

• rootMultiplicity_root (k : ι) (i : Fin self.count) (x : X) : Polynomial.rootMultiplicity (self.root i x) (P k x) = self.multiplicity k i

  The multiplicity of root i x as a root of P k x is multiplicity k i at every x.

• exists_root_eq (k : ι) (x : X) : P k x ≠ 0 → ∀ (t : ℝ), (P k x).IsRoot t → ∃ (i : Fin self.count), self.root i x = t

  Every root of a nonzero member is the value of a root function.

• exists_multiplicity_pos (i : Fin self.count) : ∃ (k : ι), 0 < self.multiplicity k i

  Every root function is a root of some member.

• eq_zero_or_ne_zero (k : ι) : (∀ (x : X), P k x = 0) ∨ ∀ (x : X), P k x ≠ 0

  Each member is the zero polynomial at every point or at none.

• natDegree_eq (k : ι) (x y : X) : (P k x).natDegree = (P k y).natDegree

  Each member has the same degree at every point.

• signInvariant_sectionSet (k : ι) (i : Fin self.count) : SignInvariant (fun (z : X × ℝ) => Polynomial.eval z.2 (P k z.1)) (sectionSet self.root i)

  Each member is sign-invariant on each section.

• signInvariant_sectorSet (k : ι) (j : Fin (self.count + 1)) : SignInvariant (fun (z : X × ℝ) => Polynomial.eval z.2 (P k z.1)) (sectorSet self.root j)

  Each member is sign-invariant on each sector.

def TauCeti.Delineation.ofRoots {X : Type u_1} {ι : Type u_3} [TopologicalSpace X] {P : ι → X → Polynomial ℝ} [PreconnectedSpace X] {n : ℕ} {θ : Fin n → X → ℝ} {m : ι → Fin n → ℕ} (hcoeff : ∀ (k : ι) (j : ℕ), Continuous fun (x : X) => (P k x).coeff j) (hnull : ∀ (k : ι), (∀ (x : X), P k x = 0) ∨ ∀ (x : X), P k x ≠ 0) (hdeg : ∀ (k : ι) (x y : X), (P k x).natDegree = (P k y).natDegree) (hθ : ∀ (i : Fin n), Continuous (θ i)) (hmono : ∀ (x : X), StrictMono fun (i : Fin n) => θ i x) (hmult : ∀ (k : ι) (i : Fin n) (x : X), Polynomial.rootMultiplicity (θ i x) (P k x) = m k i) (hroots : ∀ (k : ι) (x : X), P k x ≠ 0 → ∀ (t : ℝ), (P k x).IsRoot t → ∃ (i : Fin n), θ i x = t) (hpos : ∀ (i : Fin n), ∃ (k : ι), 0 < m k i) : Delineation P

Construct a delineation from continuous ordered roots with specified constant multiplicities. The roots must cover every nonzero member, and each section must have positive multiplicity in some member. On a preconnected base these data imply sign-invariance on all sections and sectors.

@[simp]

theorem TauCeti.Delineation.ofRoots_count {X : Type u_1} {ι : Type u_3} [TopologicalSpace X] {P : ι → X → Polynomial ℝ} [PreconnectedSpace X] {n : ℕ} {θ : Fin n → X → ℝ} {m : ι → Fin n → ℕ} (hcoeff : ∀ (k : ι) (j : ℕ), Continuous fun (x : X) => (P k x).coeff j) (hnull : ∀ (k : ι), (∀ (x : X), P k x = 0) ∨ ∀ (x : X), P k x ≠ 0) (hdeg : ∀ (k : ι) (x y : X), (P k x).natDegree = (P k y).natDegree) (hθ : ∀ (i : Fin n), Continuous (θ i)) (hmono : ∀ (x : X), StrictMono fun (i : Fin n) => θ i x) (hmult : ∀ (k : ι) (i : Fin n) (x : X), Polynomial.rootMultiplicity (θ i x) (P k x) = m k i) (hroots : ∀ (k : ι) (x : X), P k x ≠ 0 → ∀ (t : ℝ), (P k x).IsRoot t → ∃ (i : Fin n), θ i x = t) (hpos : ∀ (i : Fin n), ∃ (k : ι), 0 < m k i) : (ofRoots hcoeff hnull hdeg hθ hmono hmult hroots hpos).count = n

The delineation constructed from ordered roots has the specified number of sections.

@[simp]

theorem TauCeti.Delineation.ofRoots_root {X : Type u_1} {ι : Type u_3} [TopologicalSpace X] {P : ι → X → Polynomial ℝ} [PreconnectedSpace X] {n : ℕ} {θ : Fin n → X → ℝ} {m : ι → Fin n → ℕ} (hcoeff : ∀ (k : ι) (j : ℕ), Continuous fun (x : X) => (P k x).coeff j) (hnull : ∀ (k : ι), (∀ (x : X), P k x = 0) ∨ ∀ (x : X), P k x ≠ 0) (hdeg : ∀ (k : ι) (x y : X), (P k x).natDegree = (P k y).natDegree) (hθ : ∀ (i : Fin n), Continuous (θ i)) (hmono : ∀ (x : X), StrictMono fun (i : Fin n) => θ i x) (hmult : ∀ (k : ι) (i : Fin n) (x : X), Polynomial.rootMultiplicity (θ i x) (P k x) = m k i) (hroots : ∀ (k : ι) (x : X), P k x ≠ 0 → ∀ (t : ℝ), (P k x).IsRoot t → ∃ (i : Fin n), θ i x = t) (hpos : ∀ (i : Fin n), ∃ (k : ι), 0 < m k i) (i : Fin (ofRoots hcoeff hnull hdeg hθ hmono hmult hroots hpos).count) (x : X) : (ofRoots hcoeff hnull hdeg hθ hmono hmult hroots hpos).root i x = θ (Fin.cast ⋯ i) x

The delineation constructed from ordered roots has the specified root functions.

@[simp]

theorem TauCeti.Delineation.ofRoots_multiplicity {X : Type u_1} {ι : Type u_3} [TopologicalSpace X] {P : ι → X → Polynomial ℝ} [PreconnectedSpace X] {n : ℕ} {θ : Fin n → X → ℝ} {m : ι → Fin n → ℕ} (hcoeff : ∀ (k : ι) (j : ℕ), Continuous fun (x : X) => (P k x).coeff j) (hnull : ∀ (k : ι), (∀ (x : X), P k x = 0) ∨ ∀ (x : X), P k x ≠ 0) (hdeg : ∀ (k : ι) (x y : X), (P k x).natDegree = (P k y).natDegree) (hθ : ∀ (i : Fin n), Continuous (θ i)) (hmono : ∀ (x : X), StrictMono fun (i : Fin n) => θ i x) (hmult : ∀ (k : ι) (i : Fin n) (x : X), Polynomial.rootMultiplicity (θ i x) (P k x) = m k i) (hroots : ∀ (k : ι) (x : X), P k x ≠ 0 → ∀ (t : ℝ), (P k x).IsRoot t → ∃ (i : Fin n), θ i x = t) (hpos : ∀ (i : Fin n), ∃ (k : ι), 0 < m k i) (k : ι) (i : Fin (ofRoots hcoeff hnull hdeg hθ hmono hmult hroots hpos).count) : (ofRoots hcoeff hnull hdeg hθ hmono hmult hroots hpos).multiplicity k i = m k (Fin.cast ⋯ i)

The delineation constructed from ordered roots has the specified multiplicities.

theorem TauCeti.Delineation.nonempty_of_isEmpty {X : Type u_1} {ι : Type u_3} [TopologicalSpace X] [IsEmpty X] (P : ι → X → Polynomial ℝ) : Nonempty (Delineation P)

Any family of real polynomials over an empty base has a delineation.

theorem TauCeti.Delineation.isRoot_iff {X : Type u_1} {ι : Type u_3} [TopologicalSpace X] {P : ι → X → Polynomial ℝ} (D : Delineation P) {k : ι} {x : X} (hk : P k x ≠ 0) (t : ℝ) : (P k x).IsRoot t ↔ ∃ (i : Fin D.count), D.root i x = t ∧ 0 < D.multiplicity k i

The roots of a nonzero member of the family are exactly the values of the root functions in which it has positive multiplicity.

theorem TauCeti.Delineation.eval_ne_zero_of_mem_sectorSet {X : Type u_1} {ι : Type u_3} [TopologicalSpace X] {P : ι → X → Polynomial ℝ} (D : Delineation P) {k : ι} {j : Fin (D.count + 1)} {z : X × ℝ} (hk : P k z.1 ≠ 0) (hz : z ∈ sectorSet D.root j) : Polynomial.eval z.2 (P k z.1) ≠ 0

On a sector, the evaluation of a nonzero fiber cannot vanish: every root lies on a section, and sections are disjoint from sectors.

theorem TauCeti.Delineation.multiplicity_pos_iff {X : Type u_1} {ι : Type u_3} [TopologicalSpace X] {P : ι → X → Polynomial ℝ} (D : Delineation P) {k : ι} {i : Fin D.count} (x : X) : 0 < D.multiplicity k i ↔ P k x ≠ 0 ∧ (P k x).IsRoot (D.root i x)

A member of the family has positive multiplicity in a root function exactly when it is nonzero and vanishes there.

theorem TauCeti.Delineation.multiplicity_eq_zero {X : Type u_1} {ι : Type u_3} [TopologicalSpace X] {P : ι → X → Polynomial ℝ} (D : Delineation P) {k : ι} {x : X} (hk : P k x = 0) (i : Fin D.count) : D.multiplicity k i = 0

A member of the family that is zero somewhere has multiplicity zero in every root function.

theorem TauCeti.Delineation.range_root {X : Type u_1} {ι : Type u_3} [TopologicalSpace X] {P : ι → X → Polynomial ℝ} (D : Delineation P) (x : X) : (Set.range fun (i : Fin D.count) => D.root i x) = {t : ℝ | ∃ (k : ι), P k x ≠ 0 ∧ (P k x).IsRoot t}

At every point of the base, the values of the root functions are exactly the real roots of the nonzero members of the family.

theorem TauCeti.Delineation.biUnion_roots_toFinset_eq {X : Type u_1} {ι : Type u_3} [TopologicalSpace X] {P : ι → X → Polynomial ℝ} (D : Delineation P) [Fintype ι] (x : X) : (Finset.univ.biUnion fun (k : ι) => (P k x).roots.toFinset) = Finset.image (fun (i : Fin D.count) => D.root i x) Finset.univ

The shared distinct root set of a finite family is exactly the image of the ordered root list of its delineation. Nullified members contribute no roots.

instance TauCeti.Delineation.instSubsingleton {X : Type u_1} {ι : Type u_3} [TopologicalSpace X] {P : ι → X → Polynomial ℝ} [Nonempty X] : Subsingleton (Delineation P)

Over a nonempty base a family of real polynomials has at most one delineation: the root functions are the increasing enumeration of the real roots of the nonzero members, and the multiplicities are their root multiplicities.

def TauCeti.Delineation.comp {X : Type u_1} {Y : Type u_2} {ι : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {P : ι → X → Polynomial ℝ} (D : Delineation P) (f : Y → X) (hf : Continuous f) : Delineation fun (k : ι) (y : Y) => P k (f y)

Restriction of a delineation along a continuous map of bases.

@[simp]

theorem TauCeti.Delineation.comp_count {X : Type u_1} {Y : Type u_2} {ι : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {P : ι → X → Polynomial ℝ} (D : Delineation P) (f : Y → X) (hf : Continuous f) : (D.comp f hf).count = D.count

The restriction of a delineation has the same number of sections.

@[simp]

theorem TauCeti.Delineation.comp_root {X : Type u_1} {Y : Type u_2} {ι : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {P : ι → X → Polynomial ℝ} (D : Delineation P) (f : Y → X) (hf : Continuous f) (i : Fin (D.comp f hf).count) (y : Y) : (D.comp f hf).root i y = D.root (Fin.cast ⋯ i) (f y)

The root functions of the restriction of a delineation are the original root functions composed with the map of bases.

@[simp]

theorem TauCeti.Delineation.comp_multiplicity {X : Type u_1} {Y : Type u_2} {ι : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {P : ι → X → Polynomial ℝ} (D : Delineation P) (f : Y → X) (hf : Continuous f) (k : ι) (i : Fin (D.comp f hf).count) : (D.comp f hf).multiplicity k i = D.multiplicity k (Fin.cast ⋯ i)

The restriction of a delineation has the same multiplicities.

theorem TauCeti.nonempty_delineation {X : Type u_1} {ι : Type u_3} [TopologicalSpace X] {P : ι → X → Polynomial ℝ} [Finite ι] [PreconnectedSpace X] (hcoeff : ∀ (k : ι) (i : ℕ), Continuous fun (x : X) => (P k x).coeff i) (hnull : ∀ (k : ι), (∀ (x : X), P k x = 0) ∨ ∀ (x : X), P k x ≠ 0) (hdeg : ∀ (k : ι) (x y : X), (P k x).natDegree = (P k y).natDegree) (hcard : ∀ (k : ι) (x y : X), ((P k x).aroots ℂ).toFinset.card = ((P k y).aroots ℂ).toFinset.card) (hgcd : Pairwise fun (k l : ι) => ∀ (x y : X), (EuclideanDomain.gcd (P k x) (P l x)).natDegree = (EuclideanDomain.gcd (P k y) (P l y)).natDegree) : Nonempty (Delineation P)

Delineability from invariant fiber data. Let P k x, for k in a finite index type, be real polynomials whose coefficients depend continuously on a parameter x in a preconnected space. Suppose that each member is zero everywhere or nowhere, and that the degree of each member, its number of distinct complex roots and the degree of the gcd of every pair of distinct members do not depend on x. Then the family has a delineation.

theorem TauCeti.exists_delineation_of_isRoot_iff {X : Type u_1} [TopologicalSpace X] [PreconnectedSpace X] {F : X → Polynomial ℝ} {k : ℕ} {θ : Fin k → X → ℝ} (hcoeff : ∀ (j : ℕ), Continuous fun (x : X) => (F x).coeff j) (hdeg : ∀ (x y : X), (F x).natDegree = (F y).natDegree) (hθ : ∀ (i : Fin k), Continuous (θ i)) (hmono : ∀ (x : X), StrictMono fun (i : Fin k) => θ i x) (hroots : ∀ (x : X) (t : ℝ), (F x).IsRoot t ↔ ∃ (i : Fin k), θ i x = t) (hmult : ∀ (i : Fin k) (x y : X), Polynomial.rootMultiplicity (θ i x) (F x) = Polynomial.rootMultiplicity (θ i y) (F y)) : ∃ (D : Delineation fun (x : Unit) (x_1 : X) => F x_1), ∀ (i : Fin D.count), ∃ (j : Fin k), D.root i = θ j

Delineation from an ordered root enumeration. Let F x be real polynomials of constant degree whose coefficients depend continuously on a parameter x in a preconnected space. If continuous, pointwise strictly increasing functions θ i enumerate the real roots of every F x, each with a multiplicity independent of x, then the θ i are the root functions of a delineation of F.

theorem TauCeti.exists_delineation_ball_of_isRoot_iff {B : Type u_4} [NormedAddCommGroup B] [NormedSpace ℝ B] {F : B → Polynomial ℝ} {b₀ : B} {d k : ℕ} {s : Fin k → B → ℝ} {U : Set B} (hcoeff : ∀ᶠ (b : B) in nhds b₀, ∀ (j : ℕ), ContinuousAt (fun (b : B) => (F b).coeff j) b) (hdeg : ∀ᶠ (b : B) in nhds b₀, (F b).natDegree = d) (hU : U ∈ nhds b₀) (hs : ∀ (i : Fin k), ContinuousOn (s i) U) (hmono : ∀ b ∈ U, StrictMono fun (i : Fin k) => s i b) (hroots : ∀ b ∈ U, ∀ (t : ℝ), (F b).IsRoot t ↔ ∃ (i : Fin k), s i b = t) (hmult : ∀ b ∈ U, ∀ (i : Fin k), Polynomial.rootMultiplicity (s i b) (F b) = Polynomial.rootMultiplicity (s i b₀) (F b₀)) : ∃ ε > 0, Metric.ball b₀ ε ⊆ U ∧ ∃ (D : Delineation fun (x : Unit) (b : ↑(Metric.ball b₀ ε)) => F ↑b), ∀ (i : Fin D.count), ∃ (j : Fin k), ∀ (b : ↑(Metric.ball b₀ ε)), D.root i b = s j ↑b

Local delineation from local root data. Let F b be real polynomials over a real normed space, of constant degree near b₀, whose coefficients are continuous near b₀. Suppose that on a neighborhood U of b₀, continuous and pointwise strictly increasing functions s i enumerate the real roots of F b, with multiplicities independent of b. Then on some ball around b₀ inside U the restrictions of the s i are the root functions of a delineation of F.

Families closed under differentiation up to zero

theorem TauCeti.Delineation.root_notMem_uIcc_of_sign_eval_eq {X : Type u_1} {ι : Type u_3} [TopologicalSpace X] {P : ι → X → Polynomial ℝ} (D : Delineation P) {x : X} (hder : ∀ (k : ι), Polynomial.derivative (P k x) = 0 ∨ ∃ (l : ι), P l x = Polynomial.derivative (P k x)) {t t' : ℝ} (htt' : t ≠ t') (h : ∀ (k : ι), SignType.sign (Polynomial.eval t (P k x)) = SignType.sign (Polynomial.eval t' (P k x))) (i : Fin D.count) : D.root i x ∉ Set.uIcc t t'

Thom's lemma for delineations. Suppose that at a point x of the base the derivative of every member of the family is zero or a member. If every member has the same sign at two distinct points t ≠ t' of the fiber over x, then no root function takes a value in [t, t'] at x.

theorem TauCeti.Delineation.mk_mem_sectionSet_iff_of_sign_eval_eq {X : Type u_1} {ι : Type u_3} [TopologicalSpace X] {P : ι → X → Polynomial ℝ} (D : Delineation P) {x : X} (hder : ∀ (k : ι), Polynomial.derivative (P k x) = 0 ∨ ∃ (l : ι), P l x = Polynomial.derivative (P k x)) {t t' : ℝ} (h : ∀ (k : ι), SignType.sign (Polynomial.eval t (P k x)) = SignType.sign (Polynomial.eval t' (P k x))) (i : Fin D.count) : (x, t) ∈ sectionSet D.root i ↔ (x, t') ∈ sectionSet D.root i

Suppose that at a point x of the base the derivative of every member of the family is zero or a member. Then two points of the fiber over x at which every member has the same sign lie in the same sections.

theorem TauCeti.Delineation.mk_mem_sectorSet_iff_of_sign_eval_eq {X : Type u_1} {ι : Type u_3} [TopologicalSpace X] {P : ι → X → Polynomial ℝ} (D : Delineation P) {x : X} (hder : ∀ (k : ι), Polynomial.derivative (P k x) = 0 ∨ ∃ (l : ι), P l x = Polynomial.derivative (P k x)) {t t' : ℝ} (h : ∀ (k : ι), SignType.sign (Polynomial.eval t (P k x)) = SignType.sign (Polynomial.eval t' (P k x))) (j : Fin (D.count + 1)) : (x, t) ∈ sectorSet D.root j ↔ (x, t') ∈ sectorSet D.root j

Suppose that at a point x of the base the derivative of every member of the family is zero or a member. Then two points of the fiber over x at which every member has the same sign lie in the same sectors.

theorem TauCeti.Delineation.signInvariant_eval₂_of_mem_stackCells {A : Type u_4} [CommRing A] {n : ℕ} {φ : A →+* ℝ} {F : Finset (Polynomial (MvPolynomial (Fin n) A))} {S : Set (Fin n → ℝ)} (D : Delineation fun (p : ↥F) (x : ↑S) => Polynomial.map (MvPolynomial.eval₂Hom φ ↑x) ↑p) {f : MvPolynomial (Fin (n + 1)) A} (hf : (MvPolynomial.finSuccEquiv A n) f ∈ F) {E : Set (Fin (n + 1) → ℝ)} (hE : E ∈ stackCells S D.root) : SignInvariant (fun (y : Fin (n + 1) → ℝ) => MvPolynomial.eval₂ φ y f) E

For a delineation of the fibers of MvPolynomial.finSuccEquiv A n f over S, the polynomial f in n + 1 variables, evaluated along φ, is sign-invariant on every cell of the stack in ℝ^(n + 1).