Voronoi faces and surface-null triple strata

Intersections of distinct bisectors give the lower-dimensional triple-tie strata.

theorem LiebThirring.bisectorPlane_not_le {M : ℕ} (R : Fin M → Position) (hR : Function.Injective R) {k l p : Fin M} (hkl : k ≠ l) (hkp : k ≠ p) (hlp : l ≠ p) : ¬bisectorPlane R k l ≤ bisectorPlane R k p

Distinct bisectors with a common nucleus cannot contain one another.

theorem LiebThirring.finrank_bisectorPlane_direction {M : ℕ} (R : Fin M → Position) (hR : Function.Injective R) {k l : Fin M} (hkl : k ≠ l) : Module.finrank ℝ ↥(bisectorPlane R k l).direction = 2

theorem LiebThirring.finrank_bisectorPlane_inf_le_one {M : ℕ} (R : Fin M → Position) (hR : Function.Injective R) {k l p : Fin M} (hkl : k ≠ l) (hkp : k ≠ p) (hlp : l ≠ p) : Module.finrank ℝ ↥(bisectorPlane R k l ⊓ bisectorPlane R k p).direction ≤ 1

Each constituent of the triple stratum is an affine line, a point, or empty, as expressed by direction dimension at most one.

theorem LiebThirring.voronoiTripleStratum_eq_iUnion {M : ℕ} (R : Fin M → Position) : voronoiTripleStratum R = ⋃ (k : Fin M), ⋃ (l : { l : Fin M // k ≠ l }), ⋃ (p : { p : Fin M // k ≠ p ∧ ↑l ≠ p }), ↑(bisectorPlane R k ↑l) ⊓ ↑(bisectorPlane R k ↑p)

The triple stratum is a finite union of affine subspaces with direction dimension ≤ 1.