namespace OctonionD8
open Polynomial
theorem flow_block_diag (c s : ℝ) :
Matrix.reindex blockEquiv blockEquiv (flowMat c s) =
Matrix.fromBlocks (blockA c s) 0 0 (blockB c s) := 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
Statement. For all real numbers c,s∈R (no other hypotheses: in particular no relation such as c2+s2=1 is assumed, and c,s may be 0), the 8×8 real matrix Fc,s defined below, after its rows and columns are simultaneously permuted by the index bijection β below, equals the block-diagonal matrix
(Ac,s00Bc,s),
with the explicit 4×4 blocks Ac,s, Bc,s given below and 4×4 zero off-diagonal blocks.
The algebra. Let e0,…,e7 be the standard basis of R8 (indices 0,…,7). A bilinear product on R8 is defined by p⋅q=∑i,j,kpiqjT(i,j,k)ek, where the integer structure constants T(i,j,k) (so eiej=∑kT(i,j,k)ek) are:
e0ej=ej for all j; eie0=ei for all i (the first rule wins when i=0, giving e0e0=e0);
eiei=−e0 for i∈{1,…,7};
for distinct i,j∈{1,…,7}: the e0-coefficient is 0; and for k∈{1,…,7}, relabel i↦π(i)=(i+6)mod7=i−1∈Z/7. The Fano lines are the sets {l,l+1,l+3}⊂Z/7, l∈Z/7. Then T(i,j,k)=+1 if {π(i),π(j),π(k)} equals some line {l,l+1,l+3} and (π(i),π(j)) is one of (l,l+1), (l+1,l+3), (l+3,l); T(i,j,k)=−1 if {π(i),π(j),π(k)} is a line but the ordering is not of that form; T(i,j,k)=0 otherwise (in particular when k∈{i,j}, since then the set has only 2 elements).
Concretely, in terms of basis indices, eiej=ek for (i,j,k) any cyclic rotation of
and ejei=−ek for these, all other products of distinct imaginary units having zero coefficient.
The matrix Fc,s. For a,b∈R8, Ra is the matrix with entry (k,j) equal to the k-th coordinate of ej⋅a, i.e. the matrix (acting on column vectors, column j = image of ej) of right multiplication x↦x⋅a in the standard basis; Lb is likewise the matrix of left multiplication x↦b⋅x. Then
Fc,s=Re1+Lce1+se2,
the matrix of the linear map x↦xe1+(ce1+se2)x, with (Fc,s)k,j = the ek-coefficient of the image of ej.
The bijection and reindexing.β:{0,…,7}→{0,1,2,3}⊔{0,1,2,3} sends 0,1,2,4 to the first copy's 0,1,2,3 and 3,5,6,7 to the second copy's 0,1,2,3 (so β−1 of first-copy i is pi with (p0,p1,p2,p3)=(0,1,2,4), and of second-copy i is qi with (q0,q1,q2,q3)=(3,5,6,7)). The reindexed matrix has entry Fc,s(β−1(x),β−1(y)) at position (x,y), the same bijection being used for rows and columns. Hence the statement is equivalent to: for all i,j∈{0,1,2,3},
i.e. the coordinate subspaces span(e0,e1,e2,e4) and span(e3,e5,e6,e7) are each mapped into themselves, with the stated matrices in those ordered bases.
Confirmed by the moderator at approval.