ExampleConstruction: Literature-sourcedVerification: AI-generated

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

D4 Brink–Howlett generating graph

PDF p. 30: Figure 4; §7.2.1

Example

Use the $D_{4}$ Coxeter system with central vertex $2$ , $J = {2}$ , and simple reflections $s = s_{1}$ , $t = s_{2}$ , $u = s_{3}$ , $v = s_{4}$ . The Brink–Howlett groupoid is the quotient of the universal chamber groupoid by the normaliser quotient $N (W, J) = {Norm}_{W} (W_{J}) / W_{J}$ . Its generating graph has the four objects $1, 2, 3, 4$ , where $i$ denotes the singleton ${i}$ .

Identifying the same-coloured vertices of the universal chamber graph gives this four-object graph. Its nonloop generators are $s t : 2 \to 1$ , $t s : 1 \to 2$ , $v t : 2 \to 4$ , $t v : 4 \to 2$ , $u t : 2 \to 3$ and $t u : 3 \to 2$ . Its loops are $u, v$ at object $1$ , $s, u$ at object $4$ , and $s, v$ at object $3$ . Opposite arrows are labelled by inverse elements.

Facts & Assumptions

[F1]

The Coxeter generators $s, t, u, v$ are involutions. D4 diagram and generator conventions

[F2]

The chamber graph has the following labelled vertices and complete neighbour lists: $7 = (e, 2)$ has neighbours $4, 15, 16$ ; $4 = (s t, 1)$ has neighbours $7, 2, 6$ , with $2 = (s t u, 1)$ and $6 = (s t v, 1)$ ; $15 = (v t, 4)$ has neighbours $7, 14, 21$ , with $14 = (v t s, 4)$ and $21 = (v t u, 4)$ ; and $16 = (u t, 3)$ has neighbours $7, 10, 22$ , with $10 = (u t s, 3)$ and $22 = (u t v, 3)$ . Each adjacency gives arrows in both directions. D4 chamber labels and complete adjacency graph

[F3]

The normaliser quotient has four chamber orbits, distinguished by second labels $1, 2, 3, 4$ ; equal colours in the article's figures denote equal second labels. Four colour orbits of eight D4 chambers

[F4]

The universal groupoid arrow from $(x, I)$ to $(y, K)$ has label $x^{- 1} y$ ; adjacent crossings generate it, and reverse crossing labels are inverses. Universal groupoid interpretation of the D4 graph

[F5]

The normaliser quotient acts freely on chamber objects, and the covering to the Brink–Howlett groupoid sends $(x, I)$ to $I$ and preserves arrow labels. Its adjacent-crossing images are generators. Universal Brink–Howlett covering and its deck group

[F6]

For a free action on the objects of a connected groupoid, each arrow orbit with a given source orbit has exactly one representative with any prescribed source in that orbit. Free object actions give orbit coverings

[F7]

The normaliser quotient action is free on chamber labels and preserves adjacency and the crossing index. This applies to the finite-rank $D_{4}$ system used here. Normaliser action on labels, orbits and adjacency

Verification

Given: The $D_{4}$ data, labelled chamber graph and quotient covering in the Example.

Goal: Determine all projected crossing generators, their endpoints and inverse pairs.

1.1F2F3F4F5F6F7given

By [F3], vertices $7, 4, 16, 15$ represent the four distinct object orbits $2, 1, 3, 4$ , respectively. The covering sends each to its second label by [F5]. The universal groupoid of [F4] is nonempty, small and connected: it has the finite set of 32 chamber objects and exactly one arrow between each ordered pair. The $D_{4}$ normaliser action is free on these objects by [F7], so the orbit interface [F6] applies. Every crossing orbit has a unique representative starting at the chosen vertex for its source orbit. By [F7] the translated representative is still an adjacent crossing. Thus the complete neighbour lists in [F2] enumerate all projected crossing generators.

2.1F1F2F4step 1.1

Apply the label formula in [F4] to the three arrows out of vertex $7$ : their labels are $s t$ , $v t$ and $u t$ , with targets $1, 4, 3$ , respectively. The arrows from vertices $4, 15, 16$ back to $7$ have inverse labels $t s, t v, t u$ , respectively, by [F1] and [F4]. This gives all six nonloop arrows.

3.1F1F2F4F5step 1.1step 2.1∎

The remaining two neighbours of vertex $4$ have first components $s t u, s t v$ , so the two outgoing loop labels are $(s t)^{- 1} s t u = u$ and $(s t)^{- 1} s t v = v$ . Similarly, vertex $15$ gives $(v t)^{- 1} v t s = s$ and $(v t)^{- 1} v t u = u$ , while vertex $16$ gives $(u t)^{- 1} u t s = s$ and $(u t)^{- 1} u t v = v$ . The cancellations use the involutions in [F1]. Their endpoints have the same second labels as their sources, so these are precisely the listed loops. Together with steps 1.1 and 2.1 this proves the graph and the inverse-label assertion.

Source notes

The article reference attributes Figure 4. The verification uses the completed chamber graph and covering suppliers, rather than the attributed figure as a proof premise.

Depends on

Used by · 2

Dependency tree · 2 levels

Each result is drawn at its shortest distance from this item. Arrows run from prerequisites to the items that use them; this item has a heavier outline. External source nodes link directly to the cited text. The view shows up to two dependency steps; open a prerequisite to continue.

Sources

Normalisers of parabolic subgroups of Artin–Tits groups and Tits cone intersections · PDF p. 30, Figure 4 and §7.2.1