Hyperplane carriers are closed: the carrier $\{x : \langle n, x\rangle = d\}$ of an affine hyperplane is the preimage of a singleton under a continuous map, hence closed.
Hyperplane carriers have empty interior: if $η.carrier$ contained an open ball around some $x$, then moving $x$ slightly in the direction $η.normal$ would change the inner product $\langle η.normal, \cdot\rangle$ but stay inside the carrier — a contradiction.
Baire-style fact: a finite union of closed nowhere-dense sets has empty interior. Proof
by induction: peel off one closed set new; if some open subset $U$ of the union meets the
complement of new, $U \setminus \text{new}$ is open inside the remaining union and lies in
its interior (which is empty by IH); otherwise $U \subseteq \text{interior}\,\text{new} = \emptyset$.
Affine hyperplanes have empty interior (raw-data form): the affine hyperplane $\{x : \langle n, x\rangle = d\}$ for nonzero $n$ has empty interior. Equivalently its complement is dense; the proof shows any open set $U$ meets the complement by perturbing in the direction $n$.
The complement of an affine hyperplane is dense: equivalent reformulation of
interior_hyperplane_eq_empty via the standard duality $\text{interior}\,A = \emptyset \iff A^c$ dense.
A connected set disjoint from a hyperplane lies in one open half-space: a connected $C$ avoiding $\{\langle n, x\rangle = d\}$ is contained in $\{> d\}$ or $\{< d\}$. The two half-spaces are disjoint open sets covering $C$; preconnectedness forces $C$ into one.
Every point of the complement lies in some chamber: given $p \in arr.complement$ (i.e.
on no hyperplane), there exists a chamber $C$ containing $p$. The proof uses Zorn's lemma on
the family of connected subsets of the complement containing $p$, with the union of a chain
serving as an upper bound via IsPreconnected.sUnion_directed.
Avoidance lemma for a finite list of affine hyperplanes: given an open nonempty $V$ and a list of affine hyperplane data $(n_i, d_i)$ with $n_i \ne 0$, there exists $x \in V$ avoiding every hyperplane $\langle n_i, x\rangle = d_i$. Proof by induction on the list: at each step, intersect $V$ with the dense open complement of the next hyperplane and recurse.
Boundary point on a hyperplane belongs to the closure: if $D$ is open, $p \in D$ does
not lie on the hyperplane $\eta$, and $z$ does lie on $\eta$, then $z \in \overline{D}$. The
idea is that approaching $z$ along the segment from $p$ stays in the open half-space of $p$
and eventually inside $D$. (Currently this lemma is left as sorry.)
A wall of one chamber is also a wall of any neighboring chamber on the opposite side: if
$η$ is a wall of $C$ and $D$ contains a point $p$ on the opposite side of $η$ from $C$, then
$η$ is also a wall of $D$. The relatively open piece of $η$ extracted from the wall hypothesis
on $C$ is shown to lie in $\overline{D}$ via mem_closure_of_open_and_opposite_side.
Existence of an adjacent chamber across a wall: in a locally finite arrangement, for any
wall $η$ of a chamber $C$, there exists a chamber $D \ne C$ for which $η$ is also a wall. The
construction picks a point $q$ on $η$ in the relatively open piece, uses local finiteness to
list nearby hyperplanes, then applies avoidance_list to find a point $p'$ in the opposite
half-space avoiding all those hyperplanes. The chamber containing $p'$ (from
chamber_of_mem_complement) is the required $D$.
Uniqueness of the chamber adjacent across a wall: in a locally finite arrangement, if
two chambers $D_1, D_2$ both share the wall $η$ with $C$ and both differ from $C$, then they
must be equal. Combined with adjacent_chamber_exists this yields existence and uniqueness of
"the" adjacent chamber. (Currently this theorem is left as sorry.)