Bilinear coordinates for a ternary translation form

Abstract

Translation on a ternary group pairs opposite Fourier modes. A symmetric binary quadratic form consequently decomposes into bilinear blocks over ℤ/2ℤ.

Definition 1.1 (The translation quadratic form).

$$\forall (N:\mathbb{N}),\forall (d:\mathbb{N}),\forall (A:\mathrm{Matrix}\left(\mathrm{Fin}\left(N\right),\mathrm{Fin}\left(N\right),\mathrm{ZMod}\left(2\right)\right)),\forall (\delta :(\mathrm{Fin}\left(N\right)\to (\mathrm{Fin}\left(d\right)\to \mathrm{ZMod}\left(3\right)))),\forall (x:((\mathrm{Fin}\left(d\right)\to \mathrm{ZMod}\left(3\right))\to (\mathrm{Fin}\left(N\right)\to \mathrm{ZMod}\left(2\right)))),F\left(A,\delta ,x\right)=\sum _{(r:(\mathrm{Fin}\left(d\right)\to \mathrm{ZMod}\left(3\right)))}\sum _{(u:\mathrm{Fin}\left(N\right))}\sum _{(v:\mathrm{Fin}\left(N\right))}\mathrm{ite}\left(u<v,A\left(u,v\right)\cdot (x\left(r,u\right)\cdot x\left(r,v\right)+x\left((r+\delta (u)),u\right)\cdot x\left((r+\delta (v)),v\right)),0\right)$$

Formalization. D5/S3/QuadraticForms/TernaryTranslationQuadraticNormalForm.F (✓ std3).

Source. Repository-derived.

Commentary.

The variables are binary configurations indexed by the group Fin d → ℤ/3ℤ. For each ordered edge u < v, the form adds the original edge product to the product translated separately by δ(u) and δ(v). All sums and products in this definition take values in ℤ/2ℤ.

Definition 1.2 (The character separation matrix).

$$\forall (N:\mathbb{N}),\forall (d:\mathbb{N}),\forall (A:\mathrm{Matrix}\left(\mathrm{Fin}\left(N\right),\mathrm{Fin}\left(N\right),\mathrm{ZMod}\left(2\right)\right)),\forall (\delta :(\mathrm{Fin}\left(N\right)\to (\mathrm{Fin}\left(d\right)\to \mathrm{ZMod}\left(3\right)))),\forall (t:(\mathrm{Fin}\left(d\right)\to \mathrm{ZMod}\left(3\right))),C\left(A,\delta ,t\right)=(u:\mathrm{Fin}\left(N\right))(v:\mathrm{Fin}\left(N\right))\mapsto \mathrm{ite}\left(\sum _{(i:\mathrm{Fin}\left(d\right))}t\left(i\right)\cdot \delta (u,i)=\sum _{(i:\mathrm{Fin}\left(d\right))}t\left(i\right)\cdot \delta (v,i),0,A\left(u,v\right)\right)$$

Formalization. D5/S3/QuadraticForms/TernaryTranslationQuadraticNormalForm.C (✓ std3).

Source. Repository-derived.

Commentary.

The matrix keeps A(u,v) when the two ternary dot products differ and sets the entry to zero when they agree. Thus a character measures the separation of the two translation vectors.

Theorem 1.3 (A linear equivalence to independent blocks).

$$\forall (N:\mathbb{N}),\forall (d:\mathbb{N}),\forall (A:\mathrm{Matrix}\left(\mathrm{Fin}\left(N\right),\mathrm{Fin}\left(N\right),\mathrm{ZMod}\left(2\right)\right)),(\forall (u:\mathrm{Fin}\left(N\right)),\forall (v:\mathrm{Fin}\left(N\right)),A\left(u,v\right)=A\left(v,u\right))\Rightarrow (\forall (\delta :(\mathrm{Fin}\left(N\right)\to (\mathrm{Fin}\left(d\right)\to \mathrm{ZMod}\left(3\right)))),\forall (P:\mathrm{Finset}\left((\mathrm{Fin}\left(d\right)\to \mathrm{ZMod}\left(3\right))\right)),\neg (0\in P)\Rightarrow ((\forall (t:(\mathrm{Fin}\left(d\right)\to \mathrm{ZMod}\left(3\right))),t\ne 0\Rightarrow ((t\in P\iff \neg (-t\in P))))\Rightarrow (\exists (E:\mathrm{LinearEquiv}\left(\mathrm{ZMod}\left(2\right),((\mathrm{Fin}\left(d\right)\to \mathrm{ZMod}\left(3\right))\to (\mathrm{Fin}\left(N\right)\to \mathrm{ZMod}\left(2\right))),((\mathrm{Fin}\left(N\right)\to \mathrm{ZMod}\left(2\right))\times (\{(t:(\mathrm{Fin}\left(d\right)\to \mathrm{ZMod}\left(3\right)))\mid t\in P\}\to ((\mathrm{Fin}\left(N\right)\to \mathrm{ZMod}\left(2\right))\times (\mathrm{Fin}\left(N\right)\to \mathrm{ZMod}\left(2\right)))))\right)),\forall (x:((\mathrm{Fin}\left(d\right)\to \mathrm{ZMod}\left(3\right))\to (\mathrm{Fin}\left(N\right)\to \mathrm{ZMod}\left(2\right)))),F\left(A,\delta ,x\right)=\sum _{(t:\{(t:(\mathrm{Fin}\left(d\right)\to \mathrm{ZMod}\left(3\right)))\mid t\in P\})}\sum _{(u:\mathrm{Fin}\left(N\right))}\sum _{(v:\mathrm{Fin}\left(N\right))}((E\left(x\right)).2(t)).1(u)\cdot C\left(A,\delta ,(t).val\right)(u,v)\cdot ((E\left(x\right)).2(t)).2(v))))$$

Proof. Machine-checked in Lean as D5/S3/QuadraticForms/TernaryTranslationQuadraticNormalForm.ternary_translation_quadratic_normal_form (✓ std3). ∎

Source. Repository-derived.

Commentary.

Assume that A is symmetric and that P contains exactly one element from every opposite pair of nonzero modes. The ℤ/2ℤ-linear equivalence E has one constant-mode vector and a pair of binary vectors for each representative. The displayed sum uses precisely the first and second vectors of that pair. Fourier inversion over ℤ/2ℤ[ω], where ω² + ω + 1 = 0, constructs the equivalence; opposite modes are conjugate, and their cross terms give the bilinear blocks C(A,δ,t). No condition on the diagonal of A is required.

References

• Truth anchor: D5/S3/QuadraticForms/TernaryTranslationQuadraticNormalForm.C
• Truth anchor: D5/S3/QuadraticForms/TernaryTranslationQuadraticNormalForm.F
• Truth anchor: D5/S3/QuadraticForms/TernaryTranslationQuadraticNormalForm.ternary_translation_quadratic_normal_form