Block $A$ has characteristic polynomial $X^2(X^2 + 4)$

Proved

OctonionD8.charpoly_blockA

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

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

Then $\chi_A(X) = \det(XI - A) = X^2\,(X^2 + 4)$ .

Preamble

import Mathlib
import Definitions.Def_OctonionD8_blocks

Formal statement

namespace OctonionD8

open Polynomial

theorem charpoly_blockA (c s : ℝ) (h : c ^ 2 + s ^ 2 = 1) :
    (blockA c s).charpoly = X ^ 2 * (X ^ 2 + 4) := 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 ; 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

Theorem charpoly_blockA. Let $c, s$ be arbitrary real numbers that satisfy

c^2 + s^2 = 1 .

No other assumptions are made. $c$ and $s$ are universally quantified, and the hypothesis is satisfiable, for example by $(c,s) = (1,0)$ , $(-1,0)$ or $(0,\pm 1)$ . Every point of the unit circle is allowed, including the degenerate points $c = \pm 1$ , $s = 0$ . At $c = 1$ , $s = 0$ the entries $1-c$ and $c-1$ vanish. At $c = -1$ , $s = 0$ the entries $c+1$ and $-c-1$ vanish.

Let $A(c,s)$ be the real $4 \times 4$ matrix, with rows and columns indexed by $0,1,2,3$ , given by

A(c,s) \;=\; \begin{pmatrix} 0 & -c-1 & -s & 0 \\ c+1 & 0 & 0 & s \\ s & 0 & 0 & 1-c \\ 0 & -s & c-1 & 0 \end{pmatrix}.

This matrix is written out explicitly in the imported file. Other definitions in the same files (a block permutation of $\{0,\dots,7\}$ , a second $4\times 4$ block $B(c,s)$ , an octonion multiplication table built on the Fano plane, and an $8\times 8$ "flow" matrix) do not appear in this statement. The statement refers only to $A(c,s)$ .

The theorem asserts an equality in the polynomial ring $\mathbb{R}[X]$ :

\chi_{A(c,s)}(X) \;=\; X^2\,(X^2 + 4) \;=\; X^4 + 4X^2 .

Here $\chi_{A}(X) = \det(X I_4 - A)$ is the characteristic polynomial. This is the monic convention, computed over $\mathbb{R}[X]$ . The claimed polynomial does not depend on $c$ or $s$ . It is an equality of polynomials, meaning every coefficient matches, not just an equality of values at particular points. Over $\mathbb{C}$ its roots are $0$ with multiplicity $2$ and $\pm 2i$ , each with multiplicity $1$ .

The statement asserts nothing about the minimal polynomial, diagonalizability, eigenvectors, or about any $(c,s)$ off the unit circle.

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

Block AAA has characteristic polynomial X2(X2+4)X^2(X^2 + 4)X2(X2+4)

Block $A$ has characteristic polynomial $X^2(X^2 + 4)$