theorem AffineBuilding.sector_functional_strictly_positive_or_negative {V : Type} [DecidableEq V] (b : Building V) (S : Sector b) (eta : Wall b) (heta_apt : eta.apartment = S.apartment) : (∀ v ∈ S.vertices, 0 < eta.functional v) ∨ ∀ v ∈ S.vertices, eta.functional v < 0

A wall's defining functional is either strictly positive on all of $S$ or strictly negative on all of $S$ — sectors do not straddle walls.

theorem AffineBuilding.positive_half_apartment_canonical_side {V : Type} [DecidableEq V] {b : Building V} {S : Sector b} {eta : Wall b} {H : HalfApartment b} (heta_apt : eta.apartment = S.apartment) (hpos : IsPositiveHalfApartment S eta H) : (H.vertices = eta.halfPos ∧ ∀ v ∈ S.vertices, 0 < eta.functional v) ∨ H.vertices = eta.halfNeg ∧ ∀ v ∈ S.vertices, eta.functional v < 0

A positive half-apartment for $(S, \eta)$ is exactly one of the canonical halves eta.halfPos or eta.halfNeg, determined by the sign of $\eta$ on $S$.

theorem AffineBuilding.positive_half_apartment_unique_vertices {V : Type} [DecidableEq V] {b : Building V} {S : Sector b} {eta : Wall b} {H₁ H₂ : HalfApartment b} (heta_apt : eta.apartment = S.apartment) (hpos₁ : IsPositiveHalfApartment S eta H₁) (hpos₂ : IsPositiveHalfApartment S eta H₂) : H₁.vertices = H₂.vertices

Two positive half-apartments for the same sector and wall have the same vertex set — the positive side is canonical.

theorem AffineBuilding.parallel_sectors_positive_half_apartment_unique_vertices {V : Type} [DecidableEq V] {b : Building V} {S₁ S₂ : Sector b} {eta : Wall b} {H₁ H₂ : HalfApartment b} (hpar : Sector.SameDirection b S₁ S₂) (heta_apt₁ : eta.apartment = S₁.apartment) (heta_apt₂ : eta.apartment = S₂.apartment) (hpos₁ : IsPositiveHalfApartment S₁ eta H₁) (hpos₂ : IsPositiveHalfApartment S₂ eta H₂) : H₁.vertices = H₂.vertices

Parallel sectors $S_1 \sim S_2$ select the same positive half-apartment with respect to a fixed wall $\eta$.