Prove2Me

Block BB has characteristic polynomial (X2+2−2c)2(X^2 + 2 - 2c)^2

Proved
OctonionD8.charpoly_blockB

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

characteristic-polynomialfano-planelinear-algebraoctonions

Let c,sc, s be real with c2+s2=1c^2 + s^2 = 1, and let

B=(0−s01−cs01−c00c−10−sc−10s0).B = \begin{pmatrix} 0 & -s & 0 & 1-c \\ s & 0 & 1-c & 0 \\ 0 & c-1 & 0 & -s \\ c-1 & 0 & s & 0 \end{pmatrix}.

Then χB(X)=det⁡(XI−B)=(X2+(2−2c))2\chi_B(X) = \det(XI - B) = \bigl(X^2 + (2 - 2c)\bigr)^2.

Preamble
import Mathlib
import Definitions.Def_OctonionD8_blocks
Formal statement
namespace OctonionD8

open Polynomial

theorem charpoly_blockB (c s : ℝ) (h : c ^ 2 + s ^ 2 = 1) :
    (blockB c s).charpoly = (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 ; 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

Read-back of charpoly_blockB. Let c,sc, s be any real numbers such that

c2+s2=1.c^2 + s^2 = 1.

This is the only hypothesis. There are no other hypotheses or typeclass assumptions: everything is over R\mathbb{R}, and c,sc, s are universally quantified. Let B=B(c,s)B = B(c,s) be the real 4×44 \times 4 matrix, with rows and columns indexed by 0,1,2,30,1,2,3, defined by

B(c,s)=(0−s01−cs01−c00c−10−sc−10s0).B(c,s) = \begin{pmatrix} 0 & -s & 0 & 1-c \\ s & 0 & 1-c & 0 \\ 0 & c-1 & 0 & -s \\ c-1 & 0 & s & 0 \end{pmatrix}.

The theorem states that the characteristic polynomial of BB is the square of a quadratic. This is an equality of polynomials in one indeterminate XX with real coefficients:

χB(X)=(X2+(2−2c))2.\chi_B(X) = \bigl(X^2 + (2 - 2c)\bigr)^2 .

Here χB(X)=det⁡(XI4−B)\chi_B(X) = \det(X I_4 - B) is Mathlib's characteristic polynomial, which is monic of degree 44. The term 2−2c2 - 2c is a constant polynomial.

Hypotheses, degenerate cases, and unused definitions. The hypothesis can be satisfied. Any point (c,s)(c,s) on the unit circle works, e.g. c=cos⁡θc = \cos\theta, s=sin⁡θs = \sin\theta.

  • At (c,s)=(1,0)(c,s) = (1,0), BB is the zero matrix and the claim is χB=X4\chi_B = X^4.
  • At (c,s)=(−1,0)(c,s) = (-1,0) the claim is χB=(X2+4)2\chi_B = (X^2+4)^2.

The statement says nothing about c,sc, s off the unit circle. It does not mention any eigenvectors, the 8×88\times 8 matrices, the octonion multiplication table, or the index bijection Fin 8≃Fin 4⊔Fin 4\mathrm{Fin}\,8 \simeq \mathrm{Fin}\,4 \sqcup \mathrm{Fin}\,4 ("blockEquiv"), which are all defined in the imported files. It also does not mention the companion 4×44\times 4 matrix "blockA". None of these appear in the statement. The only imported definition it uses is the explicit matrix B(c,s)B(c,s) shown above.

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