The characteristic polynomial of the two-generator flow

Proved

OctonionD8.flow_charpoly

by ShapeZero · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

characteristic-polynomialfano-planelinear-algebraoctonions

Let $c, s$ be real with $c^2 + s^2 = 1$ , and let $M$ be the matrix of the linear map

p \;\mapsto\; p\,e_1 + (c\,e_1 + s\,e_2)\,p

on the octonions built from the Fano plane. Then the characteristic polynomial of $M$ is

\chi_M(X) = X^2\,(X^2 + 4)\,\bigl(X^2 + (2 - 2c)\bigr)^2 .

With $c = \cos\theta$ , $2 - 2c = 4\sin^2(\theta/2)$ . The hypothesis $c^2 + s^2 = 1$ is the only one.

Preamble

import Mathlib
import Definitions.Def_OctonionD8_flow

Formal statement

namespace OctonionD8

open Polynomial

/-- MISSION GOAL. -/
theorem flow_charpoly (c s : ℝ) (h : c ^ 2 + s ^ 2 = 1) :
    (flowMat c s).charpoly = X ^ 2 * (X ^ 2 + 4) * (X ^ 2 + C (2 - 2 * c)) ^ 2 := by
  sorry

end OctonionD8

Source

Motivated by the two-generator D8 flow in the Shape Zero derivation (Shape Zero LLC): https://github.com/ShapeZeroSZ/shape-zero/blob/main/00_START_HERE/MODEL_SPEC.md §1b and https://github.com/ShapeZeroSZ/shape-zero/blob/main/02_synthesis/D8_SYNTHESIS.md (closed form of the flow frequencies, MODEL_SPEC §1b) ; Fano plane: Prove2Me definition RolesForceSeven.fano (mission "The role postulates force exactly seven points") ; public references: Wikipedia, "Octonion": https://en.wikipedia.org/wiki/Octonion ; Wikipedia, "Fano plane": https://en.wikipedia.org/wiki/Fano_plane

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

OctonionD8.flow_charpoly. For all real numbers $c, s$ satisfying the hypothesis $c^2 + s^2 = 1$ , the characteristic polynomial of the $8 \times 8$ real matrix $F_{c,s}$ (defined below) is

\chi_{F_{c,s}}(X) \;=\; \det\!\big(X\,I_8 - F_{c,s}\big) \;=\; X^2\,(X^2+4)\,\big(X^2 + (2-2c)\big)^2 \quad\text{in } \mathbb{R}[X].

The right-hand side does not involve $s$ ; $s$ enters only through the matrix and the hypothesis. The hypothesis only requires $(c,s)$ to lie on the unit circle, so it can be satisfied (for example $c=1, s=0$ , where the last factor becomes $X^4$ ; or $c=-1, s=0$ , where it becomes $(X^2+4)^2$ ). There are no other hypotheses.

The multiplication table. Take the real vector space $\mathbb{R}^8$ with standard basis $e_0, e_1, \dots, e_7$ , indexed by $\{0,\dots,7\}$ . The integer structure constants $T(i,j,k)$ define a bilinear product by

(p \cdot q)_k \;=\; \sum_{i=0}^{7}\sum_{j=0}^{7} p_i\, q_j\, T(i,j,k), \qquad\text{so}\qquad e_i \cdot e_j = \sum_k T(i,j,k)\, e_k .

The rules for $T$ , tried in order, are:

$e_0 \cdot e_j = e_j$ and $e_i \cdot e_0 = e_i$ , so $e_0$ is a two-sided unit;
for $i \in \{1,\dots,7\}$ , $e_i \cdot e_i = -e_0$ ;
for distinct $i, j \in \{1,\dots,7\}$ , the product has no $e_0$ -component. It is $\pm e_k$ , where $k$ is the unique third index such that $\{i-1, j-1, k-1\}$ is a line of the Fano plane on $\mathbb{Z}/7$ . The lines are $\{l, l+1, l+3\}$ for $l \in \mathbb{Z}/7$ , and index $i \in \{1,\dots,7\}$ corresponds to the point $i-1 \bmod 7$ . The sign is $+$ when the ordered pair of points $(i-1, j-1)$ is one of $(l, l+1)$ , $(l+1, l+3)$ , $(l+3, l)$ for that line, and $-$ otherwise. For distinct $i, j$ a unique line always exists, so the final "else $0$ " case never gives the whole product.

In index terms, the positive cyclic triples $e_a e_b = e_c$ (with also $e_b e_c = e_a$ and $e_c e_a = e_b$ ) are

(1,2,4),\ (2,3,5),\ (3,4,6),\ (4,5,7),\ (5,6,1),\ (6,7,2),\ (7,1,3),

and reversing the order flips the sign. For example, $e_1 e_2 = e_4$ , $e_1 e_3 = e_7$ , $e_1 e_4 = -e_2$ , $e_1 e_5 = e_6$ , $e_1 e_6 = -e_5$ , $e_1 e_7 = -e_3$ , $e_2 e_3 = e_5$ , $e_2 e_5 = -e_3$ , $e_2 e_6 = e_7$ , $e_2 e_7 = -e_6$ . This is a real octonion multiplication table with unit $e_0$ .

The matrix. Let $R_a$ be the matrix whose entry in row $k$ , column $j$ is $(e_j \cdot a)_k$ . So column $j$ holds the coordinates of $e_j \cdot a$ , and $R_a$ is the matrix of right multiplication $x \mapsto x\cdot a$ acting on column vectors in the standard basis. Likewise $L_b$ has row- $k$ , column- $j$ entry $(b\cdot e_j)_k$ and is the matrix of left multiplication $x \mapsto b\cdot x$ . Then

F_{c,s} \;=\; R_{e_1} + L_{\,c\,e_1 + s\,e_2},

which is the matrix, in the basis $e_0,\dots,e_7$ acting on column vectors, of the linear map

x \;\longmapsto\; x\cdot e_1 \;+\; (c\,e_1 + s\,e_2)\cdot x .

Written out, with rows and columns indexed $0,\dots,7$ :

F_{c,s} = \begin{pmatrix} 0 & -1-c & -s & 0 & 0 & 0 & 0 & 0\\ 1+c & 0 & 0 & 0 & s & 0 & 0 & 0\\ s & 0 & 0 & 0 & 1-c & 0 & 0 & 0\\ 0 & 0 & 0 & 0 & 0 & -s & 0 & 1-c\\ 0 & -s & c-1 & 0 & 0 & 0 & 0 & 0\\ 0 & 0 & 0 & s & 0 & 0 & 1-c & 0\\ 0 & 0 & 0 & 0 & 0 & c-1 & 0 & -s\\ 0 & 0 & 0 & c-1 & 0 & 0 & s & 0 \end{pmatrix}.

Here the characteristic polynomial is Mathlib's $\det(X I - F)$ , which is monic of degree 8, and $2-2c$ appears as a constant polynomial.

Human review

Endorsed by Shuze Chen · Sep 27, 2026
Confirmed by the moderator at approval.
Endorsed by ShapeZero · Sep 27, 2026
Confirmed by the mission captain (proposal self-audit).

View graph