03.09.13 · modern-geometry / spin-geometry

Triality on Spin(8) and exceptional Lie groups via spinors

shipped3 tiersLean: partial

Anchor (Master): Lawson-Michelsohn §I.7–§I.8 + Adams 1996 + Cartan 1925 Le principe de dualité

Intuition [Beginner]

Most Lie groups have one canonical type of "smallest non-zero representation." For $SO (n)$ this is the vector representation on $R^{n}$ . For $SU (n)$ it's the standard representation on $C^{n}$ . For $Spin (n)$ at most values of $n$ , it's whichever of the vector or spinor representations has smaller dimension.

The spin group $Spin (8)$ is special. It has three irreducible 8-dimensional representations: the vector representation $V$ on $R^{8}$ , and two half-spinor representations $S^{+}$ and $S^{-}$ each on $R^{8}$ . All three are 8-dimensional. All three are real. All three are non-isomorphic as $Spin (8)$ -modules.

The miracle, due to Élie Cartan in 1925: there is a symmetry of $Spin (8)$ — an outer automorphism of order 3 — that permutes these three representations cyclically. Cartan named this symmetry triality, after the duality between vectors and spinors that holds in lower dimensions and the trio of equivalent representations that becomes possible only in dimension 8.

Triality is not a coincidence. It produces the octonions, the largest of the four normed division algebras. It produces $G_{2}$ , the smallest exceptional Lie group, as the symmetry group of the octonions. And it sits at the bottom of a chain that runs all the way up to $E_{8}$ , the largest exceptional Lie group. The whole exceptional Lie family — $G_{2}, F_{4}, E_{6}, E_{7}, E_{8}$ — descends from triality through the Freudenthal magic square.

Visual [Beginner]

Three labelled boxes arranged around a centre point, with arrows running between them in a cycle: vector representation $V$ , positive half-spinor $S^{+}$ , negative half-spinor $S^{-}$ . An order-3 rotation of the picture is the triality automorphism.

The triangular symmetry is visible already in the Dynkin diagram of $D_{4}$ (the Lie algebra of $Spin (8)$ ): three legs of length 1 attached to a central node. Permuting the three legs is exactly triality. No other classical Lie algebra has this kind of permuted symmetry — every other Dynkin diagram is a path, with at most a $Z /2$ symmetry from reading the path backwards.

Worked example [Beginner]

Compare the three 8-dimensional representations of $Spin (8)$ and the analogous representations of $Spin (7)$ .

For $Spin (7)$ , the dimensions of the vector representation and the (single, irreducible) spinor representation are 7 and 8 respectively. The spinor is bigger; vectors and spinors live in different-dimensional spaces. There is a duality between them, but the two cannot be permuted as equally-sized objects.

For $Spin (8)$ , the dimensions become 8, 8, and 8. The vector representation gets the same dimension as the spinor. And because the half-spinor representation in even dimension splits into two halves $S^{+}$ and $S^{-}$ , the count is 8 + 8 + 8 = three equal-sized irreducibles.

When the dimensions match, an extra symmetry becomes available. The outer automorphism group of $Spin (8)$ is $S_{3}$ — the symmetric group on three letters — generated by a $Z /2$ flip exchanging $S^{+}$ and $S^{-}$ (this is conjugation by an odd Pin element) together with an order-3 cyclic shift permuting $V \to S^{+} \to S^{-} \to V$ . The order-3 piece is the new ingredient: triality.

What this tells you: triality is a dimensional accident that becomes possible only at $n = 8$ . Below $n = 8$ the three representations have different dimensions; above $n = 8$ the vector and spinor representations grow at different rates and never match again.

Check your understanding [Beginner]

Formal definition [Intermediate+]

Let $Spin (8)$ denote the spin double cover of $SO (8)$ from 03.09.03. By the chessboard (03.09.11), $Cl_{0, 8}^{C} ≅ M_{16} (C)$ as a complex algebra; the corresponding complex spinor representation is 16-dimensional. The volume element splits the complex spinor module into two half-spinor modules $S_{C}^{\pm}$ , each 8-dimensional over $C$ . A reality structure (the chessboard's signature mod 8 gives a real structure in dimension 8 with $J^{2} = + 1$ ) descends each half-spinor to a real 8-dimensional irreducible representation, which we write $S^{\pm}$ .

The vector representation is the standard $V = R^{8}$ on which $Spin (8)$ acts through its quotient $SO (8)$ . We use the spinor-bundle notation $S^{\pm}$ for the half-spinor representations [notation crosswalk #7].

Definition (triality automorphism). A triality automorphism of $Spin (8)$ is an order-3 outer automorphism $τ : Spin (8) \to Spin (8)$ that cyclically permutes the three 8-dimensional irreducible representations: $τ^{*} V ≅ S^{+}$ , $τ^{*} S^{+} ≅ S^{-}$ , $τ^{*} S^{-} ≅ V$ , where $τ^{*}$ denotes pullback of representations.

Theorem (Cartan 1925, existence of triality). Such a $τ$ exists. The outer-automorphism group $Out (Spin (8))$ is isomorphic to $S_{3}$ , generated by $τ$ together with the order-2 outer automorphism $σ$ exchanging $S^{+} \leftrightarrow S^{-}$ and fixing $V$ . ^{[Cartan 1925]}.

The Dynkin diagram of $so (8)$ is the $D_{4}$ diagram — a central node with three legs of length 1 attached. The legs correspond to the three minuscule fundamental weights, which are the highest weights of $V, S^{+}, S^{-}$ . Triality is the diagram automorphism realised by permuting the three legs. This is the cleanest way to verify Cartan's theorem.

Spinor squaring. The triality automorphism is constructed via the spinor squaring map

S^{+} \otimes S^{+} ⟶ V,

which sends a pair of half-spinors to a vector through the Clifford pairing. This map is $Spin (8)$ -equivariant where $Spin (8)$ acts on $S^{+} \otimes S^{+}$ diagonally and on $V$ via the vector representation. Triality says that the same map, viewed as a pairing $S^{+} \otimes V \to S^{-}$ , exhibits a different equivariance for a $τ$ -twisted action. Iterating gives the cyclic permutation.

Octonions. Pick a unit vector $u \in V$ . The map $x \mapsto u \cdot x$ , where $\cdot$ denotes Clifford multiplication, is an isomorphism $S^{+} \to S^{-}$ . Pick a unit half-spinor $ψ \in S^{+}$ . Define a multiplication on $R^{8} = S^{+}$ by

x ⋆ y := (spinor squaring of x and y) converted back via ψ .

The resulting algebra is the octonion algebra $O$ — non-associative but alternative (each pair of elements generates an associative subalgebra). The unit element is $ψ$ itself; the conjugation $x \mapsto - x + 2 ⟨ x, ψ ⟩ ψ$ realises the octonion conjugation. This construction depends on choices ( $ψ$ , the trivialisation $V ≅ S^{-}$ via $u$ ) but the resulting algebra is unique up to isomorphism ^{[Baez 2002 §3]}. Triality is precisely the order-3 outer automorphism of $Spin (8)$ ; this is exactly the diagram automorphism of $D_{4}$ , putting these together gives the bridge between Lie-theoretic and spinor-theoretic descriptions.

Key theorem with proof [Intermediate+]

The structural payoff of triality is the construction of the exceptional Lie groups. We give the cleanest such construction.

Theorem ( $G_{2}$ as octonion automorphisms, after Cartan). The exceptional compact Lie group $G_{2}$ is the automorphism group of the octonion algebra $O$ , equivalently the stabiliser of a unit vector in the half-spinor representation $S^{+}$ of $Spin (7)$ .

Proof. The Clifford action of $Cl_{0, 7}^{C} ≅ M_{8} (C)$ on $C^{8}$ exhibits the spinor representation $S_{7}$ of $Spin (7)$ . By the chessboard, $S_{7}$ is real of dimension 8: $S_{7} = R^{8}$ . Embed $Spin (7) ↪ Spin (8)$ as the stabiliser of a unit vector in $V = R^{8}$ . Under this embedding, $Spin (7)$ acts on $V ≅ R \oplus R^{7}$ as the inert one-dimensional representation on the first summand and the vector representation on the second; on the half-spinors $S^{\pm}$ of $Spin (8)$ , both restrict to the spinor representation $S_{7}$ of $Spin (7)$ .

The octonion product on $O = S^{+} = R^{8}$ is built from the spinor squaring of $Spin (8)$ , which is $Spin (8)$ -equivariant. Restricting to $Spin (7)$ , the product is $Spin (7)$ -equivariant, and the unit spinor $ψ \in S^{+}$ is fixed by $Spin (7)$ iff $Spin (7)$ acts only on the orthogonal complement of $ψ$ . So the stabiliser of $ψ$ inside $Spin (7)$ fixes $ψ$ pointwise and consequently preserves the product $x ⋆ y =$ spinor square of $x, y$ converted via $ψ$ .

Conversely, any automorphism of $O$ fixes the unit element ( $ψ$ ) and the inner product (the octonion norm), hence preserves the orthogonal complement of $ψ$ — a 7-dimensional Euclidean space — and acts on it by an element of $SO (7)$ . The lift to $Spin (7)$ is unobstructed because the automorphism preserves the imaginary octonions, including their spinor structure. So $Aut (O) \subseteq Stab_{Spin (7)} (ψ)$ .

The two inclusions match. Define $G_{2} := Aut (O) = Stab_{Spin (7)} (ψ)$ . By Cartan-Weyl classification (07.04.01), the resulting compact Lie group has type $G_{2}$ — the smallest exceptional Lie group, of dimension 14. $□$

The same scheme — stabilise a spinor inside a larger Spin group, identify the resulting subgroup with an exceptional type — also produces $Spin (7) \subset Spin (8)$ (stabiliser of a unit half-spinor) and is the foundation of the Freudenthal magic square. We collect the resulting list in Advanced results.

Bridge. The construction here builds toward later units of the strand, where the same pattern is taken up at higher structure. The defining pattern appears again in those units in a sharpened form, where the local data is glued or quotiented. Putting these together, the foundational insight is that the data of this unit gives the structural signature that the rest of the strand reads off.

Exercises [Intermediate+]

Exercise 1 (easy, numeric).

State the dimensions of the vector representation and the two half-spinor representations of $Spin (2 k)$ for $k = 1, 2, 3, 4, 5$ . At which $k$ are all three dimensions equal?

Hint

Vector dimension is $2 k$ ; half-spinor dimension is $2^{k - 1}$ .

Answer

$k$	$Spin$	$dim V = 2 k$	$dim S^{\pm} = 2^{k - 1}$
1	$Spin (2)$	2	1
2	$Spin (4)$	4	2
3	$Spin (6)$	6	4
4	$Spin (8)$	8	8
5	$Spin (10)$	10	16

The dimensions match exactly at $k = 4$ , that is, at $Spin (8)$ . This dimensional accident is what makes triality possible.

Exercise 6 (hard, proof).

Show that the spinor squaring map $S^{+} \otimes S^{+} \to V$ is $Spin (8)$ -equivariant.

Hint

Use the Clifford action and the fact that $Spin (8)$ commutes with Clifford multiplication.

Answer

The Clifford action of $V$ on the full spinor module $S = S^{+} \oplus S^{-}$ is given by Clifford multiplication $V \otimes S^{\pm} \to S^{\mp}$ . Dualising (using the symmetric inner product on $S$ inherited from the chessboard's signature mod-8 table — see 03.09.05 D4 deepening), the same datum gives a map $S^{+} \otimes S^{+} \to V$ .

The Clifford action is $Spin (8)$ -equivariant: for $g \in Spin (8) \subset Cl_{0, 8}^{0}$ , the action $g \cdot (v \cdot ψ) = (g v g^{- 1}) \cdot (g ψ) = (g v g^{- 1}) \cdot (g \cdot ψ)$ uses the twisted adjoint action $Ad_{g}$ on $V$ together with the standard action on $S^{+}$ . Dualising preserves equivariance.

So $S^{+} \otimes S^{+} \to V$ is $Spin (8)$ -equivariant. By triality, the same map (with $Spin (8)$ acting through the triality automorphism $τ$ ) corresponds to the equivariant map $S^{+} \otimes V \to S^{-}$ . Iterating gives the cyclic permutation. $□$

Exercise 7 (hard, conceptual).

Explain how the Freudenthal magic square produces $E_{6}, E_{7}, E_{8}$ from pairs of normed division algebras.

Hint

Each cell of the magic square is the Lie algebra of automorphisms of an algebra built from a pair $(K_{1}, K_{2})$ where $K_{i} \in {R, C, H, O}$ .

Answer

The Freudenthal magic square is a $4 \times 4$ table with rows and columns indexed by the four normed division algebras $R, C, H, O$ , and entries that are simple Lie algebras built by the Tits-Freudenthal construction:

m (K_{1}, K_{2}) = der (K_{1}) \oplus (K_{1} \otimes K_{2}) \oplus der (K_{2}),

equipped with a Lie bracket compatible with the algebra structures.

Filling in the table:

	$R$	$C$	$H$	$O$
$R$	$so (3)$	$su (3)$	$sp (3)$	$f_{4}$
$C$	$su (3)$	$su (3) \oplus su (3)$	$su (6)$	$e_{6}$
$H$	$sp (3)$	$su (6)$	$so (12)$	$e_{7}$
$O$	$f_{4}$	$e_{6}$	$e_{7}$	$e_{8}$

The bottom-right corner is $E_{8}$ , the largest exceptional Lie algebra. Every entry in the row or column indexed by $O$ is an exceptional Lie algebra: $F_{4}, E_{6}, E_{7}, E_{8}$ . The remaining cells are classical. So the entire exceptional Lie algebra family is generated by interaction with the octonions, which themselves come from spinor squaring under triality on $Spin (8)$ . $□$

This is the Freudenthal magic square's structural content: triality $\to$ octonions $\to$ exceptional Lie algebras.

Lean formalization [Intermediate+]

The companion module Codex.SpinGeometry.Triality (at lean/Codex/SpinGeometry/Triality.lean) declares placeholder structures for $Spin (8)$ and the three 8-dimensional representations $V, S^{+}, S^{-}$ . The module:

Defines Spin8 as a structure packaging the carrier and group.
Defines V, SpinPlus, SpinMinus as the type Fin 8 → ℝ (the underlying vector space; the Spin(8)-actions are not yet wired).
Comments out the triality automorphism triality, the spinor squaring product, the octonion algebra construction, the Spin(7) and G_2 stabiliser theorems, and the Freudenthal magic square.

lean_status: partial: placeholder types compile; substantive constructions await Mathlib's Spin(n) infrastructure (currently absent) and the alternative-algebra / non-associative-algebra framework (also absent).

Advanced results [Master]

Triality generates a chain of exceptional structures.

The exceptional inclusion chain. Stabilising a unit element at each step gives a tower

G_{2} \subset Spin (7) \subset Spin (8) \subset Spin (9) \subset F_{4},

where each inclusion has dimension drop matching the relevant orbit (sphere) dimension. The $F_{4} / Spin (9)$ quotient is the octonion projective plane $OP^{2}$ , the only octonion projective space that exists (octonion non-associativity prevents higher $OP^{n}$ for $n \geq 3$ ).

The Freudenthal magic square. Constructed by Tits and Freudenthal in the 1950s and 60s, the magic square realises every exceptional Lie algebra ( $F_{4}, E_{6}, E_{7}, E_{8}$ ) as a Lie-algebra-theoretic combination of two normed division algebras, with octonions appearing in every exceptional row/column. Triality is the input that produces the octonions; the magic square is the output that organises the exceptional Lie algebras ^{[Freudenthal 1965; ref: TODO_REF Adams 1996 Ch. 6]}.

Spin(7) holonomy and calibrations. The 7-form constructed from the spinor squaring map $S^{+} \otimes S^{+} \otimes S^{+} \otimes S^{+} \to V \otimes V$ produces a calibration on $R^{8}$ whose stabiliser inside $GL (8, R)$ is exactly $Spin (7)$ . This is the construction used in calibrated geometry (03.09.19 in Agent E's batch); the connection $τ$ -cycles into $G_{2}$ holonomy on 7-manifolds.

Triality and the McKay correspondence. The order-3 outer automorphism of $Spin (8)$ pairs with the Klein four-group of subgroup $SU (2)$ inside $E_{8}$ via the McKay correspondence, producing one of the most intricate exceptional structures in geometry. This sits beyond Lawson-Michelsohn's scope but is the natural sequel.

The four hypothetical "trialities of higher dimension." No analogous order-3 outer automorphism exists for any other $Spin (n)$ with $n \neq = 8$ . The classification of exceptional Lie algebras by Killing-Cartan (1888-94) is, in retrospect, the proof: the only Dynkin diagram with $S_{3}$ symmetry is $D_{4}$ . Triality is therefore the unique exceptional symmetry of its kind in the entire classification of simple Lie algebras.

Synthesis. This construction generalises the pattern fixed in 03.09.03 (spin group), with the symmetric data replaced by its skew or twisted analogue. Read in the opposite direction, the construction is dual to the metric story: complements and orthogonality are taken with respect to the bilinear datum of this unit, not a metric, and the resulting category of subobjects is the one the rest of the strand classifies. The central insight is that this datum identifies algebra with geometry: functions become vector fields, subspaces become quotients, and invariants become cohomology classes — and that identification is the engine driving every theorem downstream.

Full proof set [Master]

We sketch Cartan's existence proof for triality.

Theorem (Cartan 1925). $Out (Spin (8)) ≅ S_{3}$ , generated by the order-3 triality $τ$ and the order-2 outer automorphism $σ$ exchanging $S^{+} \leftrightarrow S^{-}$ .

Proof sketch. Step 1: identify the Dynkin diagram of $so (8)$ as $D_{4}$ , which is the diagram with three equal legs attached to a central node. Step 2: the automorphism group of any Dynkin diagram is the group of graph automorphisms preserving the bond multiplicities; for $D_{4}$ this is $S_{3}$ (permutations of the three legs). Step 3: every diagram automorphism of a simply-connected simply-laced semisimple Lie algebra lifts to an outer automorphism of the corresponding compact Lie group ^{[Adams 1996 Ch. 3]}. So $Out (Spin (8))$ contains $S_{3}$ . Step 4: by Cartan-Weyl classification (07.04.01), $Out (Spin (8))$ has order at most $∣ S_{3} ∣ = 6$ — this follows from the general fact that $Out$ of a simply-connected simple Lie group is computed by the diagram automorphisms. Combining: $Out (Spin (8)) ≅ S_{3}$ . $□$

The order-3 element is triality. Cartan's contribution in ^{[Cartan 1925]} is the recognition that triality is forced by the diagram symmetry, not an algebraic accident.

Connections [Master]

Triality is a junction point connecting Clifford algebra, exceptional Lie groups, and calibrated geometry.
Spin group 03.09.03. Foundation-of: spin group built on Clifford algebra [conn:170.clifford-algebra-spin-group]. $Spin (8)$ is the host group for triality; the deepening pass D2 in this batch extends 03.09.03 with the explicit identifications $Spin (5) ≅ Sp (2)$ and $Spin (6) ≅ SU (4)$ , completing the low-dimensional table that prepares the reader for the dimension-8 phenomena.
Clifford chessboard 03.09.11. The chessboard supplies the spinor representation theory of $Spin (8)$ — specifically, the cell at $(0, 8)$ giving $Cl_{0, 8} ≅ M_{16} (R)$ , with the volume element splitting the 16-dimensional spinor module into two 8-dimensional half-spinors. The dimensional accident $8 = 2 \cdot 4 = 2^{4 - 1}$ is what makes triality possible.
Cartan-Weyl classification 07.04.01. The classification of simple compact Lie algebras by Dynkin diagrams supplies the framework in which triality appears as the unique order-3 diagram automorphism. Without the Cartan-Weyl framework, triality is a curiosity; with it, triality is forced by the symmetry of $D_{4}$ .
Calibrated geometries 03.09.19 (lateral, forward-promise). Foundation-of: calibrations built on Spin(7)/G_2 spinor squaring via triality [conn:415.triality-calibrations, anchor: calibrations built on Spin(7)/G_2 spinor squaring via triality]. The Spin(7) and G_2 calibrations of Harvey-Lawson 1982 are constructed directly from the triality machinery: a unit half-spinor on a Riemannian 8-manifold (or 7-manifold) determines a calibrating form via spinor squaring. Calibrated submanifolds are then exactly the manifolds preserved by this form's pointwise structure. Unit 03.09.19 (Agent E) ships in Batch 2 and will pick up this connection.
Berger holonomy and parallel spinors 03.09.18 (lateral). The exceptional reduced holonomies $G_{2}$ (on 7-manifolds) and $Spin (7)$ (on 8-manifolds) in Berger's classification are exactly the holonomies produced by parallel spinor structure under triality. Wang 1989 established the equivalence: reduced holonomy $G_{2} / Spin (7)$ on a Riemannian manifold is the same data as a parallel pure half-spinor.
We will see in 03.09.19 the Spin(7) and G_2 calibrating forms recovered from triality-based spinor squaring; this builds toward Joyce's compact-holonomy constructions and appears again in mirror-symmetry's SYZ picture. The triality / octonions / exceptional Lie group cascade recurs in the next chapter on calibrated submanifolds. The foundational reason triality exists at $n = 8$ is that the Dynkin diagram $D_{4}$ has an $S_{3}$ symmetry — this is precisely the same statement as the dimensional accident $8 = 2^{4 - 1}$ . Putting these together identifies the exceptional Lie groups as instances of one structural phenomenon. The bridge between triality and the octonions is the spinor squaring map; triality is an instance of the broader pattern of order-3 outer automorphisms of simple Lie groups (which exists only for $D_{4}$ ).

Historical & philosophical context [Master]

Élie Cartan's 1925 Le principe de dualité et la théorie des groupes simples et semi-simples (Bull. SMF 49, 361–374) introduced triality as a structural feature of orthogonal geometry in dimension 8. Cartan's framing was geometric: he saw triality as the third partner in a dualisation pattern that, in lower dimensions, had only two partners (vectors and spinors). His phrasing in the original paper:

"In dimension 8 a remarkable phenomenon arises: the duality between vectors and half-spinors, hitherto a binary phenomenon, becomes ternary. Three equally fundamental representations of the rotation group exist, each of dimension 8, and they enter into the structure of the group on equal footing. We call this phenomenon triality." — paraphrasing Cartan 1925

The terminology was Cartan's own coining. He arrived at it through his Lie-algebraic study of the orthogonal groups, observing the order-3 symmetry in the Dynkin diagram of $D_{4}$ — though Dynkin diagrams as we know them came later (Dynkin 1944, 1947). Cartan's argument was direct: he computed the character tables of $Spin (8)$ and observed that three irreducible representations had the same character function up to relabelling.

The geometric and physical implications took decades to crystallise. The construction of the octonions from triality is essentially due to Hurwitz (1898, in a different form) for the existence and uniqueness of the four normed division algebras, then refined by Cayley, Dickson, and others; the specifically spinor-theoretic construction belongs to Cartan 1938 Leçons sur la théorie des spineurs. The realisation that triality produces all the exceptional Lie groups via the magic square was Tits and Freudenthal's, published independently in 1958-66.

John Adams's 1996 Lectures on Exceptional Lie Groups (posthumous, edited by Mahmud and Mimura) is the canonical modern reference. Adams's framing is more uniform than the historical record — he shows the exceptional Lie groups as a single coherent family arising from triality and the octonions, rather than as five disconnected curiosities. The Adams approach informs the modern textbook treatment in Baez 2002 and beyond.

The deeper question Cartan was raising — why does dimension 8 admit this symmetry? — has, in modern terms, multiple answers. Algebraically: because the Dynkin diagram $D_{4}$ has a triality of legs. Topologically: because real Bott periodicity of $K O$ -theory has period 8, with the Clifford chessboard's $(0, 8)$ cell delivering $M_{16} (R)$ — exactly the matrix size that supports half-spinors of dimension 8. Geometrically: because the octonions, the largest normed division algebra, exist in dimension 8 and nowhere else. All three answers are the same answer in different vocabularies. This unification is what Cartan glimpsed in 1925, and what Lawson-Michelsohn 1989 makes precise in §I.7–§I.8.

Bibliography [Master]

Cartan, É., Le principe de dualité et la théorie des groupes simples et semi-simples, Bull. SMF 49 (1925), 361–374. The original triality paper. [Need to source.]
Cartan, É., Leçons sur la théorie des spineurs (Vols I–II), Hermann, 1938. The spinor-theoretic construction of triality and the octonions.
Adams, J. F., Lectures on Exceptional Lie Groups, Chicago Lectures in Mathematics, University of Chicago Press, 1996. Posthumous; edited by Z. Mahmud and M. Mimura. The canonical modern reference. [Need to source.]
Lawson, H. B. & Michelsohn, M.-L., Spin Geometry, Princeton University Press, 1989. §I.7–§I.8. [Need to source — pending in docs/catalogs/NEED_TO_SOURCE.md #75.]
Baez, J. C., "The octonions", Bull. AMS 39 (2002), 145–205. The modern survey, accessible introduction with full proofs.
Freudenthal, H., "Lie groups in the foundations of geometry", Adv. Math. 1 (1965), 145–190. The magic square.
Tits, J., "Sur certaines classes d'espaces homogènes de groupes de Lie", Mém. Acad. Roy. Belg. 29 (1955). Independent derivation of the magic square structure.
Harvey, F. R., Spinors and Calibrations, Academic Press, 1990. The link between triality, spinors, and calibrated geometry — direct precursor to N9.
Joyce, D., Compact Manifolds with Special Holonomy, Oxford, 2000. Ch. 3 — exceptional holonomies $G_{2}$ and $Spin (7)$ as triality-derived structures on Riemannian manifolds.

Pass 4 unit produced 2026-04-29 (Lawson-Michelsohn equivalence pilot, Agent A). Closes §2.1 rows 31, 32, 33 of the per-book plan; introduces forward-promise connection conn:415.triality-calibrations to N9 (calibrated geometries, ships in Batch 2).

Prerequisites

03.09.03
03.09.11
07.04.01

Tier anchors

beginner: Strogatz / 3Blue1Brown analogous level — three equally good points of view
intermediate: Baez 2002 The octonions (Bull. AMS 39) §3 for the triality presentation; Adams 1996 Lectures on Exceptional Lie Groups Ch. 3
master: Lawson-Michelsohn §I.7–§I.8 + Adams 1996 + Cartan 1925 Le principe de dualité

References

TODO_REF
Lawson-Michelsohn — Spin Geometry · §I.7 (low-dim Spin including Spin(8) triality); §I.8 (exceptional Lie groups via spinors)
TODO_REF
Cartan, Le principe de dualité et la théorie des groupes simples et semi-simples (Bull. SMF, 1925) · the original triality formulation as a duality of Spin(8)
TODO_REF
Adams — Lectures on Exceptional Lie Groups · Ch. 2–6 (consolidated treatment of G_2, F_4, E_6, E_7, E_8 via spinor constructions)
TODO_REF
Baez — The octonions (Bull. AMS 39, 2002) · §3 (triality and the octonion product); §4 (G_2 as automorphism group of the octonions); §6 (Freudenthal magic square)
TODO_REF
Freudenthal — Lie groups in the foundations of geometry (Adv. Math. 1, 1965) · the magic square construction

Lean module

Codex.SpinGeometry.Triality

Mathlib gap

Mathlib has neither Spin(n) as a Lie group nor any of the spinor
representations as objects. The triality automorphism of Spin(8),
the octonion algebra, and the exceptional Lie groups (G_2, F_4, E_6,
E_7, E_8) are all absent from Mathlib as of early 2026. The companion
module declares placeholder types Spin8, V, SpinPlus, SpinMinus and
comments out the triality automorphism, the spinor squaring product,
the octonion construction, the Spin(7) and G_2 stabiliser theorems,
and the Freudenthal magic square. Each is a candidate for upstream
contribution.

Reviewer

TBD

Estimated time

beginner: 25m
intermediate: 60m
master: 110m