Instances For
Instances For
Instances For
Reflection through a unit vector: when $\|e\| = 1$, the formula for the linear reflection across the hyperplane $e^\perp$ simplifies to $v \mapsto v - 2\langle e, v\rangle\,e$, since the denominator $\langle e, e\rangle = \|e\|^2 = 1$ disappears.
Coroot of a unit vector: when $\|e\| = 1$, the coroot $e^\vee = 2e/\langle e, e\rangle$ simplifies to $2e$.
Dihedral root system from two unit vectors: given two non-parallel unit vectors $e, f$ with the Cartan-integrality condition $2\langle e, f\rangle \in \mathbb{Z}$, there exists a crystallographic root system containing $e$ and $f$ such that no root is parallel to $e - f$. This is the geometric construction of a dihedral root system in the span of two wall normals.
Minimality of $e$ and $f$ in their chamber (cf. Section 12.3 of the Buildings textbook): starting from a generic functional $v_0$ that is positive on $e$ and gives equal values to $e$ and $f$, we can find a refined $v$ such that $\langle v, e\rangle = \langle v, f\rangle$ is the minimum positive value of $\langle v, \cdot\rangle$ on the root system. Geometrically, this means $e$ and $f$ are minimal positive roots (i.e. simple roots) with respect to $v$.
Generic vector in the hyperplane $d^\perp$: given a nonzero $d$ and a finite set $S$ of
nonzero vectors none of which is parallel to $d$, there exists $v \in d^\perp$ (i.e.
$\langle v, d\rangle = 0$) such that $\langle v, \gamma\rangle \ne 0$ for every $\gamma \in S$.
The proof projects $S$ onto $d^\perp$ along $d$ to obtain a nonzero set $S'$, then applies
exists_inner_ne_zero_of_finite_nonzero to find a vector $u$ avoiding all kernels in $S'$, and
finally $v = \pi_{d^\perp}(u)$ works by self-adjointness of the projection.
Existence of a chamber functional witnessing simplicity of $e$ and $f$: under the
assumption that no root is parallel to $e - f$, we construct a vector $v$ generic for the root
system, taking positive equal values on $e$ and $f$, and minimal positive value precisely on $e$
(and $f$). This functional $\gamma \mapsto \langle v, \gamma\rangle$ will witness $e$ and $f$ as
simple roots. The proof first finds $w \perp (e - f)$ that is generic for the roots via
exists_in_ker_inner_ne_zero, flips sign if needed, then applies
minimality_from_section_12_3.
Identifying $e$ and $f$ as positive multiples of simple roots: given the dihedral root
system from dihedral_orbit_root_system, we exhibit a generic linear functional $g$ together
with simple roots $\alpha, \beta$ such that $e = c_\eta \alpha$ and $f = c_\zeta \beta$ for some
positive scalars $c_\eta, c_\zeta$ (in fact here $c_\eta = c_\zeta = 1$ and $\alpha = e$,
$\beta = f$). Proof: pick $v$ from exists_chamber_functional_for_roots, take
$g = \langle v, \cdot\rangle$, and verify the simple-root property directly using minimality.
Cartan integrality of inward unit normals in a Coxeter arrangement: for two walls $\eta, \zeta$ of a chamber $C$ in a Coxeter arrangement, the inner product of their inward unit normals satisfies $2\langle e_\eta, e_\zeta\rangle \in \mathbb{Z}$. This packages the finite-order property of the rotation $s_\eta s_\zeta$ into a Cartan integer. The four sign cases (positive vs negative half-space for each wall) are handled by tracking the appropriate sign in front of the integer $n$ from the locally-finite assumption.
Linear independence of two non-parallel unit vectors: if $e, f$ are unit vectors with $f$
not a scalar multiple of $e$, then $\{e, f\}$ is linearly independent. Using linearIndependent_fin2
this reduces to showing $e \ne 0$ (immediate from $\|e\| = 1$) and that no $f = a \cdot e$
relation holds, which contradicts h_not_parallel.
Constructive identification of inward unit normals as simple roots: for two distinct,
non-parallel walls of a chamber in a Coxeter arrangement, we construct a crystallographic root
system $\Phi$ and a generic functional $f$ such that the inward unit normals are positive
multiples of simple roots $\alpha, \beta$. The construction chains together
coxeter_arrangement_dihedral_finite, linearIndependent_of_unit_not_parallel,
dihedral_orbit_root_system, and dihedral_simple_root_identification.
Wall normals are simple roots (public-facing version): a direct restatement of
wall_normals_are_simple_roots_construction exposing the same conclusion without separate
proof. This is the primary external API used by nonparallel_walls_inner_nonpos.
Non-parallel walls have non-positive inner product of inward normals: when two walls of a
chamber in a Coxeter arrangement have non-parallel inward unit normals, the inner product
$\langle e_\eta, e_\zeta\rangle \le 0$. This follows by identifying the normals as positive
multiples of simple roots via wall_normals_are_simple_roots, then applying
simple_roots_inner_nonpos_axiom to conclude.
Closure passes from a strict half-space to a closed half-space: if $S$ is contained in the
open half-space $\{x : \langle n, x\rangle > a\}$, then its closure is contained in the closed
half-space $\{x : \langle n, x\rangle \ge a\}$. This is a routine application of
closure_minimal using continuity of the inner product.
A wall meets the closure of its chamber: if $\eta$ is a wall of $C$, then the hyperplane
carrier $\eta$ intersects the closure of $C$ non-trivially. Direct unpacking of the definition
IsWall.
Hyperplane equation and chamber half-space in terms of the inward unit normal: for a wall $\eta$ of chamber $C$, there is a real number $a$ such that the carrier of $\eta$ equals $\{y : \langle e_\eta, y\rangle = a\}$ and the chamber lies in the strict half-space $\{y : \langle e_\eta, y\rangle > a\}$. The constant $a$ is obtained by rescaling $\eta$'s offset by $\|η.normal\|^{-1}$ and adjusting sign according to which half-space $C$ lies in.
Inner product of inward unit normals of distinct walls is non-positive (without the
non-parallel hypothesis): this is the geometric heart of the Coxeter property. We split into
the parallel and non-parallel cases. In the parallel case $f = c \cdot e$ with $|c| = 1$, so
$c = 1$ (impossible, since it would force $\eta.carrier = \zeta.carrier$ — contradicted using
closure_subset_closedHalfSpace and wall_carrier_meets_closure) or $c = -1$ (giving
$\langle e, f\rangle = -1 \le 0$). In the non-parallel case, this reduces to
nonparallel_walls_inner_nonpos.