periodicExternalTTNormalEquationGeneratorMatrixEntry5
plain-language theorem explainer
Matrix entry for the external transverse-traceless normal-equation generator on the encoded 5×5×5 periodic Freudenthal torus. Rows run over external edges; columns 0–124 are conformal vertex deltas and 125–499 are longitudinal vertex-component generators. Cited when matching Lean certificate skeletons to the Python payload generators. Defined by a direct case split on the column index.
Claim. On the encoded $5\times 5\times 5$ periodic Freudenthal torus, for each external edge index $e$ and column $c\in\mathbb{N}$, the generator-matrix entry $A_{e,c}\in\mathbb{R}$ is $\frac12(\mathbf{1}_{c=b}+\mathbf{1}_{c=h})$ when $c<125$ (with $b,h$ the base and head vertex indices of $e$), and equals the signed difference of the edge displacement coordinate on the corresponding longitudinal gauge component when $c\ge 125$.
background
Track 1.D opens the tensor/shear sector of the weak-field metric. The older Track 1.B conformal ansatz puts one scalar potential at each vertex and averages endpoint values onto edges; 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 (125 vertices). External edges carry base and head vertex indices in the numerical order $v=(x\cdot 5+y)\cdot 5+z$. Columns split into a conformal block of length 125 and a longitudinal gauge block of length $125\cdot 3=375$ (total width 500), matching the Python payload generators used by certificate skeletons.
proof idea
Pure definition, no proof obligations. Decode the external edge from its encoded index, read base and head vertex indices, then case on the column: if $c<125$, emit the averaged conformal incidence $(\mathbf{1}{c=\mathrm{base}}+\mathbf{1}{c=\mathrm{head}})/2$; otherwise peel off the gauge offset $c-125$, split into vertex index and Cartesian component via integer division/modulo by 3, and emit the signed difference of the edge displacement coordinate at head minus base (zero when the gauge vertex is neither endpoint).
why it matters
Supplies the single-entry kernel for the external TT normal-equation generator matrix that the Python certificate payloads already use. The immediate consumer is the row-wise matrix-vector product that dots an arbitrary coefficient vector of length 500 against one selected edge row; that product is the Lean-side counterpart of the generated certificate skeletons. In the broader Recognition gravity track this is scaffolding for the shear/TT sector beyond the conformal ansatz, needed before one can claim coverage of transverse-traceless weak-field modes on the discrete torus. It does not yet close any forcing-chain landmark (T0–T8); it is infrastructure for the gravity analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.