Points off all hyperplanes lie in some open half-space of each: if $x$ is in
arr.complement (i.e. on no hyperplane of arr), then for any hyperplane $η$, $x$ is in
either $η.positiveHalfSpace$ or $η.negativeHalfSpace$.
Positive half-space is open: convenience alias for HalfSpaceOpen η.
Negative half-space is open: $\{x : \langle n, x\rangle < d\}$ is open as the preimage of $(-\infty, d)$ under the continuous map $x \mapsto \langle n, x\rangle$.
Open half-spaces are disjoint: positive and negative open half-spaces of any hyperplane are disjoint.
Negative half-space is convex: parallel to HalfSpaceConvex for the positive side;
direct verification with positive convex combinations preserving the strict inequality.
A preconnected subset of the complement that contains a point in the positive half-space of $η$ is entirely contained in that half-space: since $S$ is covered by two disjoint open sets $η.positive$ and $η.negative$, preconnectedness forces $S$ into the one that contains the witness $x$.
Dual of connected_subset_in_positive: a preconnected subset of the complement that
contains a point in the negative half-space of $η$ is entirely contained in that half-space.
A chamber lies entirely in one open half-space of every hyperplane: a basic structural
fact about chambers; combines complement_mem_halfSpace at a witness point with
connected_subset_in_positive/negative.
The hyperplane $η$ separates two chambers $C, D$: each of the two open half-spaces of $η$ contains exactly one of $C, D$.
Instances For
The chambers $C$ and $D$ are on the same side of $η$: both lie in the positive half-space, or both lie in the negative half-space.
Instances For
Trichotomy fails — only same-side or separated: for any hyperplane $η$, two chambers
$C, D$ are either on the same side of $η$ or strictly separated by $η$. Immediate four-way
case split on chamber_subset_halfSpace.
Two chambers are adjacent along $η$: they are distinct, are separated by $η$, and lie on the same side of every other hyperplane. This is the natural geometric notion of "differing only by a single wall reflection".
Instances For
Adjacency of chambers: there exists some hyperplane $η$ of arr along which $C$ and $D$
are adjacent.
Instances For
A point of the complement lying on the correct side of every hyperplane belongs to $C$: if for each hyperplane $η$, $x$ shares $C$'s sign, then $x \in C.set$. Proof: take the segment from some $y \in C$ to $x$; convexity of half-spaces shows the segment avoids every hyperplane, so $C \cup \text{segment}$ is connected in the complement, and maximality of $C$ forces $x \in C$.
Two chambers on the same side of every hyperplane are equal: a converse to the
trichotomy. Two Subset.antisymm applications, each using mem_chamber_of_same_signs to
deduce that a point of one chamber lies in the other.
The first hyperplane crossed by a path from $C$ to $D$ is a wall of $C$: for two
distinct chambers in a locally finite arrangement, there exists a hyperplane $η$ that is both
a wall of $C$ and separates $C$ from $D$. This is the geometric heart of producing walls from
distinctness. (Currently this theorem is left as sorry.)
Wall separation theorem: a public-facing restatement of
first_crossed_hyperplane_isWall — for distinct chambers $C, D$ in a locally finite
arrangement, some wall of $C$ separates $C$ from $D$.
No chamber is in both half-spaces simultaneously: if $C$ were contained in both $η.positive$ and $η.negative$, any witness point would have $\langle n, x\rangle > d$ and $< d$ — contradiction.
Adjacent chambers are separated by exactly one wall: if $C, D$ are adjacent along $η$,
then the only hyperplane separating them is $η$ itself. A four-way case split on the
half-space sides; in each case chamber_not_both_sides yields a contradiction.
Converse to adjacent_separated_by_unique_wall: if $η$ separates $C, D$ and is the
unique separating hyperplane, then $C$ and $D$ are adjacent along $η$.
Hyperplane carrier is closed (in-namespace alias): the carrier $\{x : \langle n, x\rangle = d\}$ is closed as the preimage of $\{d\}$ under a continuous map.
The complement of a locally finite arrangement is open: for a locally finite arrangement
arr, the set $E \setminus arr.unionSet$ is open. Near each $x$, only finitely many
hyperplanes meet a small ball; intersecting the ball with the complements of those finitely
many closed carriers gives an open neighborhood of $x$ contained in the complement.
Chambers are open in a locally finite arrangement: take a ball around $x \in C$ inside
arr.complement (using complement_isOpen); then $C \cup \text{ball}$ is connected in the
complement, so by the maximality of $C$ the entire ball lies in $C$.