Root-count characterizations of stack cells

For a strictly ordered finite stack, a point is on section i exactly when its height is one of the section values and exactly i section values are below it. It is in sector j exactly when its height is not a section value and exactly j section values are below it. These descriptions identify stack cells with uniform polynomial shared-root formulas. The order-theoretic statements allow any linearly ordered height type and include the empty stack and both unbounded sectors.

theorem TauCeti.mem_sectionSet_iff_mem_image_card_lt {X : Type u_1} {α : Type u_2} [LinearOrder α] {k : ℕ} {θ : Fin k → X → α} (i : Fin k) (z : X × α) (hθ : StrictMono fun (l : Fin k) => θ l z.1) : z ∈ sectionSet θ i ↔ z.2 ∈ Finset.image (fun (l : Fin k) => θ l z.1) Finset.univ ∧ {x ∈ Finset.image (fun (l : Fin k) => θ l z.1) Finset.univ | x < z.2}.card = ↑i

A section is characterized by membership in the finite set of section heights and the number of section heights strictly below the point. Indices are counted from zero.

theorem TauCeti.mem_sectorSet_iff_notMem_image_card_lt {X : Type u_1} {α : Type u_2} [LinearOrder α] {k : ℕ} {θ : Fin k → X → α} (j : Fin (k + 1)) (z : X × α) (hθ : StrictMono fun (l : Fin k) => θ l z.1) : z ∈ sectorSet θ j ↔ z.2 ∉ Finset.image (fun (l : Fin k) => θ l z.1) Finset.univ ∧ {x ∈ Finset.image (fun (l : Fin k) => θ l z.1) Finset.univ | x < z.2}.card = ↑j

A sector is characterized by avoiding the finite set of section heights and the number of section heights strictly below the point. This includes the empty stack.

theorem TauCeti.image_cylinder_sectionSet_eq_setOf_mem_card_lt {α : Type u_2} [LinearOrder α] {k n : ℕ} {S : Set (Fin n → α)} {θ : Fin k → ↑S → α} (Z : (Fin n → α) → Finset α) (hZ : ∀ (x : ↑S), Z ↑x = Finset.image (fun (l : Fin k) => θ l x) Finset.univ) (hθ : ∀ (x : ↑S), StrictMono fun (l : Fin k) => θ l x) (i : Fin k) : cylinder S '' sectionSet θ i = {y : Fin (n + 1) → α | Fin.tail y ∈ S} ∩ {y : Fin (n + 1) → α | y 0 ∈ Z (Fin.tail y) ∧ {x ∈ Z (Fin.tail y) | x < y 0}.card = ↑i}

A section in ambient coordinates is the cylinder over the base intersected with its finite-height membership and rank condition. The height set need agree with the stack only on the base.

theorem TauCeti.image_cylinder_sectorSet_eq_setOf_notMem_card_lt {α : Type u_2} [LinearOrder α] {k n : ℕ} {S : Set (Fin n → α)} {θ : Fin k → ↑S → α} (Z : (Fin n → α) → Finset α) (hZ : ∀ (x : ↑S), Z ↑x = Finset.image (fun (l : Fin k) => θ l x) Finset.univ) (hθ : ∀ (x : ↑S), StrictMono fun (l : Fin k) => θ l x) (j : Fin (k + 1)) : cylinder S '' sectorSet θ j = {y : Fin (n + 1) → α | Fin.tail y ∈ S} ∩ {y : Fin (n + 1) → α | y 0 ∉ Z (Fin.tail y) ∧ {x ∈ Z (Fin.tail y) | x < y 0}.card = ↑j}

A sector in ambient coordinates is the cylinder over the base intersected with its finite-height nonmembership and rank condition, including the unbounded sectors.