periodicConformalGenerator5_relativeColumn_eq_shift
plain-language theorem explainer
On the 5×5×5 periodic Freudenthal torus, a row-frame relative reindexing of a conformal generator column equals the same generator evaluated after a global vertex shift by the row base. Anyone assembling translation-covariant conformal or TT normal-equation generators on the discrete torus cites this. The proof rewrites both sides at endpoints and simplifies with the relative-column endpoint equalities.
Claim. Let $E$ be the edge set of the canonical $5\times 5\times 5$ periodic Freudenthal torus, and let $v$ be a vertex index. For edges $\mathrm{row},\mathrm{col}\in E$, the conformal generator column at $v$ evaluated on the row-frame relative column of $\mathrm{col}$ equals the conformal generator column at the vertex obtained by translating $v$ by the base of $\mathrm{row}$, evaluated on $\mathrm{col}$.
background
Track 1.D builds the tensor/shear sector beyond the Track 1.B conformal ansatz. That ansatz assigns one scalar potential per vertex and induces edge-length variations by averaging endpoint potentials; it cannot represent pure shear, so it misses transverse-traceless gravitational-wave modes. This module separates independent edge perturbations from vertex-conformal ones and records elementary rectangle obstructions.
The ambient lattice is the canonical encoded $5\times 5\times 5$ periodic Freudenthal torus (PeriodicTorus5), with edges PeriodicEdge5. The conformal generator attaches to each vertex index a column over edges: its support is read off the two encoded endpoints of an edge. A row-frame relative column reindexes one edge relative to another's base; a global translate shifts vertex indices by that base. The identity equates those two ways of moving a conformal column.
proof idea
Term proof in two steps. First rewrite both sides with the endpoint evaluation rule for the conformal generator, so each side becomes a comparison of whether the (relative or absolute) edge meets the given vertex at its first or second endpoint. Then simp closes the goal using the two relative-column endpoint characterizations: the first (resp. second) encoded endpoint of the relative column equals a vertex iff the corresponding endpoint of the absolute column equals the globally translated vertex. No case split or induction is required.
why it matters
Translation covariance of conformal generator columns is the discrete gauge bookkeeping needed before combining conformal and shear data into normal equations. The sole recorded consumer is the companion identity for combined TT normal-equation generators: a row-frame translate of any combined normal-equation generator column is exactly the globally shifted combined generator column. That parent lifts the same relative-column/shift pattern from the pure conformal slice to the full Track 1.D generator stack used for weak-field tensor modes on the periodic torus. Within the gravity track this is scaffolding for shear-capable discrete gravity, not a forcing-chain (T0–T8) landmark; it keeps conformal columns consistent under the torus translation action so later TT analyses do not pick a preferred origin.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.