Column (i,j) maps bijectively to i*q+j<N; rows (ell,k,coordinate) biject with 14*n positions. Construct all tables from beta traces.
Method: native-induction. Induction: table length. Risk: routine.
This is a human-readable planning contract, not a parsed kernel formula or accepted proof.