Proposition 46, p. 31 — the coset complex of Theorem 45 has dimension d − 1, is good and has no empty squares

Let $F$ be a finite group, $d > 1$, and $H_1, \dots, H_d \le F$ subgroups such that

1. $\big(\bigcap_{j \neq i} H_j\big) \setminus H_i \neq \emptyset$ for every $i \in [d]$, and
2. the coset complex $C = C_F(H_1, \dots, H_d)$ contains no empty square.

Then $C$ has dimension $d - 1$, is good (finite, pure, properly colorable with $d$ colors, and satisfies replacement), and has no empty squares.

This is the step that turns the group-theoretic construction of Theorem 45 into a good complex, from which Proposition 42 produces a $d$-dimensional pseudo-cube.

Formalization Note The hypotheses are exactly "as in Theorem 45". The dimension is $d - 1$ with natural-number subtraction, which is exact because $d > 1$; the coloring then takes values in Fin (d - 1 + 1), i.e. $d$ colors.