The reordered basis and the two blocks of the flow matrix
DefinitionOctonionD8_blocksThe reordering. blockEquiv is the bijection from the indices to two copies of that sends to positions of the first block and to positions of the second: the basis order .
The blocks. For real ,
intended as the blocks of the flow matrix on and on .
Formalization Note blockEquiv : Fin 8 ≃ Fin 4 ⊕ Fin 4; blockA c s and blockB c s are explicit Matrix (Fin 4) (Fin 4) ℝ.
import Mathlib
import Definitions.Def_OctonionD8_flow
namespace OctonionD8
/-- Reordering of the basis e₀, …, e₇ as (e₀, e₁, e₂, e₄ | e₃, e₅, e₆, e₇):
indices 0, 1, 2, 4 go to the first block, 3, 5, 6, 7 to the second, in that order. -/
def blockEquiv : Fin 8 ≃ Fin 4 ⊕ Fin 4 where
toFun := ![Sum.inl 0, Sum.inl 1, Sum.inl 2, Sum.inr 0, Sum.inl 3, Sum.inr 1, Sum.inr 2, Sum.inr 3]
invFun := Sum.elim ![0, 1, 2, 4] ![3, 5, 6, 7]
left_inv := by decide
right_inv := by decide
/-- The block of `flowMat c s` on (e₀, e₁, e₂, e₄). -/
def blockA (c s : ℝ) : Matrix (Fin 4) (Fin 4) ℝ := !![0, -c - 1, -s, 0;
c + 1, 0, 0, s;
s, 0, 0, 1 - c;
0, -s, c - 1, 0]
/-- The block of `flowMat c s` on (e₃, e₅, e₆, e₇). -/
def blockB (c s : ℝ) : Matrix (Fin 4) (Fin 4) ℝ := !![0, -s, 0, 1 - c;
s, 0, 1 - c, 0;
0, c - 1, 0, -s;
c - 1, 0, s, 0]
end OctonionD8
Read-back
What the Lean code literally says, in plain math · claude-opus-5-5
Conventions. All three declarations live in the namespace OctonionD8. Indices of are and indices of are (zero-based, exactly as in the code). None of the three definitions refers to anything from the imported files (the octonion table, , , , , the Fano plane); they are written out by hand with explicit literal entries.
blockEquiv. This is a bijection
where the target is the disjoint union of two copies of , a "left" copy (written ) and a "right" copy (written ). The forward map is the explicit table
So the left block consists of the indices (in that order, becoming left-indices ) and the right block consists of the indices (in that order, becoming right-indices ). The inverse map is
and the two inverse laws are checked by exhaustive computation. Note that the order within each block is increasing, but the split is not "first four / last four": index goes to the right block and index to the left block.
blockA. For arbitrary real numbers (no relation between them is assumed; in particular is not required), is the real matrix whose entry in row , column () is given by
rows listed top to bottom as and columns left to right as . Entry by entry, the nonzero entries are
and all other entries () are . As written, for all (the matrix is skew-symmetric for every ). Degenerate values: at the only nonzero entries are , ; at the only nonzero entries are , .
blockB. For arbitrary real numbers (again unconstrained), is the real matrix with rows top to bottom and columns left to right:
Entry by entry, the possibly nonzero entries are
and all other entries () are . As written, for all (skew-symmetric for every ). Degenerate values: at , is the zero matrix; at the nonzero entries are and .
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.