periodicExternalTTNormalEquationGeneratorMatrixDot5
plain-language theorem explainer
Sparse row-dot of the external transverse-traceless normal-equation generator matrix on the canonical 5×5×5 periodic Freudenthal torus. Given a coefficient map and one edge index, it returns the finite sum of coefficients times the corresponding matrix entries. Certificate skeletons that mirror the Python assembly cite this Lean-side counterpart. The body is a plain sum over 500 columns.
Claim. On the canonical $5\times 5\times 5$ periodic Freudenthal torus, for a coefficient map $c:\mathbb{N}\to\mathbb{R}$ and an edge index $e$, the external TT normal-equation generator-matrix row-dot is $\sum_{k=0}^{499} c(k)\,A_{e,k}$, where $A_{e,k}$ is the external generator-matrix entry at that edge and column.
background
Track 1.D opens the tensor/shear sector of the weak-field metric. Track 1.B's conformal ansatz puts one scalar potential at each vertex and varies edge lengths by averaging endpoint potentials; that scalar slice cannot represent pure shear, so it misses transverse-traceless gravitational-wave modes. This module separates independent edge perturbations from vertex-conformal ones and records the elementary rectangle obstruction for the conformal ansatz.
The ambient lattice is the canonical encoded $5\times 5\times 5$ periodic Freudenthal torus. The external generator matrix is the Lean counterpart of the Python matrix used by generated certificate skeletons; each selected row is sparse (two conformal endpoint terms plus the three possible longitudinal component differences). The present definition packages the row-vector product against an arbitrary coefficient map.
proof idea
Pure definition: a finite sum over Fin 500 of coeff col * the corresponding external generator-matrix entry at the chosen edge index. No lemmas are applied; the body is definitionally the sparse matrix-vector product for one selected row.
why it matters
Fills the Lean-side matrix-dot primitive that certificate skeletons expect when checking the external TT normal equations on the $5^3$ torus. Without an explicit row-dot, the shear-sector assembly cannot be compared termwise to the Python generators that drive the Track 1.D certificates. It sits inside the larger program of lifting weak-field gravity beyond the conformal ansatz toward genuine transverse-traceless modes (the gap flagged in the module doc). No downstream theorems yet consume it; it is infrastructure for those certificates rather than a forcing-chain landmark (T0–T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.