Gerzon equality without dimension congruence restrictions

Abstract

At Gerzon equality, the equiangular parameters satisfy a² = (d + 2)b over every field of characteristic different from two and in every dimension at least two.

Theorem 1.1 (Pairing a linear combination with an equiangular vector).

$$\forall (F:Type\ast ),\forall (S:Type\ast ),[\mathrm{Field}\left(F\right)][\mathrm{AddCommGroup}\left(S\right)][\mathrm{Module}\left(F,S\right)]\forall (n:\mathbb{N}),\forall (K:\mathrm{LinearMap}.\mathrm{BilinForm}(F,S)),\forall (P:(\mathrm{Fin}\left(n\right)\to S)),\forall (a:F),\forall (b:F),(\forall (i:\mathrm{Fin}\left(n\right)),\forall (j:\mathrm{Fin}\left(n\right)),K\left(P\left(i\right),P\left(j\right)\right)=\mathrm{if}\left(i=j,a^2,b\right))\Rightarrow (\forall (t:(\mathrm{Fin}\left(n\right)\to F)),\forall (j:\mathrm{Fin}\left(n\right)),K\left(\sum _{i:\mathrm{Fin}\left(n\right)}(\mathrm{smul}\left(t\left(i\right),P\left(i\right)\right)),P\left(j\right)\right)=(a^2-b)\cdot t\left(j\right)+b\cdot (\sum _{i:\mathrm{Fin}\left(n\right)}t\left(i\right)))$$

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

Source. Repository-derived.

Commentary.

A bilinear form with constant diagonal value a squared and constant off-diagonal value b pairs a linear combination with its j-th vector by separating the j-th coefficient from the sum of all coefficients. The scalar field and the module are arbitrary; neither symmetry nor nondegeneracy is needed.

Theorem 1.2 (Nonzero constant trace gives linear independence).

$$\forall (F:Type\ast ),\forall (S:Type\ast ),[\mathrm{Field}\left(F\right)][\mathrm{AddCommGroup}\left(S\right)][\mathrm{Module}\left(F,S\right)]\forall (n:\mathbb{N}),\forall (K:\mathrm{LinearMap}.\mathrm{BilinForm}(F,S)),\forall (tau:\mathrm{LinearMap}\left(F,S,F\right)),\forall (P:(\mathrm{Fin}\left(n\right)\to S)),\forall (a:F),\forall (b:F),(\forall (i:\mathrm{Fin}\left(n\right)),\forall (j:\mathrm{Fin}\left(n\right)),K\left(P\left(i\right),P\left(j\right)\right)=\mathrm{if}\left(i=j,a^2,b\right))\Rightarrow ((\forall (i:\mathrm{Fin}\left(n\right)),\mathrm{tau}\left(P\left(i\right)\right)=a)\Rightarrow ((a^2\ne b)\Rightarrow ((a\ne 0)\Rightarrow (\mathrm{LinearIndependent}\left(F,P\right)))))$$

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

Source. Repository-derived.

Commentary.

Suppose a linear functional takes the same nonzero value a on every vector, while a bilinear form takes value a squared on the diagonal and b off the diagonal, with a squared different from b. Applying the functional to a linear relation makes the coefficient sum vanish. Pairing that relation with each vector then makes every coefficient vanish. No symmetry, nondegeneracy or dimension assumption is required.

Definition 1.3 (Equiangular systems).

$$\forall (F:\mathrm{Type}),[\mathrm{Field}\left(F\right)]\forall (d:\mathbb{N}),\forall (n:\mathbb{N}),\forall (B:\mathrm{LinearMap}.\mathrm{BilinForm}(F,(\mathrm{Fin}\left(d\right)\to F))),\forall (\phi :(\mathrm{Fin}\left(n\right)\to (\mathrm{Fin}\left(d\right)\to F))),\forall (a:F),\forall (b:F),\mathrm{IsEquiangularSystem}\left(B,\phi ,a,b\right)=((\forall (j:\mathrm{Fin}\left(n\right)),B\left(\phi (j),\phi (j)\right)=a)\wedge (\forall (i:\mathrm{Fin}\left(n\right)),\forall (j:\mathrm{Fin}\left(n\right)),(i\ne j)\Rightarrow (B{\left(\phi (i),\phi (j)\right)}^2=b)))$$

Formalization. D5/S3/QuadraticForms/GerzonEqualityParameterIdentity.IsEquiangularSystem (✓ std3).

Citation. Gary R. W. Greaves, Joseph W. Iverson, John Jasper, Dustin G. Mixon (2021). Frames over finite fields: Equiangular lines in orthogonal geometry. DOI: 10.48550/arXiv.2012.13642. URL: https://arxiv.org/abs/2012.13642v2.

Commentary.

Definition 2.8, page 5: “Let Φ = {ϕⱼ}ⱼ∈[n] be a sequence of vectors in a quadratic space W over F_q. For a, b ∈ F_q, Φ is called an (a, b)-equiangular system if: (i) ⟨ϕⱼ, ϕⱼ⟩ = a for every j ∈ [n], (ii) ⟨ϕᵢ, ϕⱼ⟩² = b for every i ≠ j in [n].” The sequence is represented by φ : Fin n → Fin d → F, the pairing by B, and the field parameters by a and b. Fin n indexes n vectors from zero; [n] in the paper indexes the same number from one. The predicate is polymorphic in the field and does not require its finiteness.

Definition 1.4 (The unrestricted parameter identity).

$$\mathrm{claim}=(\forall (F:\mathrm{Type}),[\mathrm{Field}\left(F\right)][\mathrm{Fintype}\left(F\right)](\mathrm{ringChar}\left(F\right)\ne 2)\Rightarrow (\forall (d:\mathbb{N}),(2\le d)\Rightarrow (\forall (B:\mathrm{LinearMap}.\mathrm{BilinForm}(F,(\mathrm{Fin}\left(d\right)\to F))),(B.\mathrm{IsSymm})\Rightarrow ((B.\mathrm{Nondegenerate})\Rightarrow (\forall (\phi :(\mathrm{Fin}\left(\mathrm{Nat}.\mathrm{choose}((d+1),2)\right)\to (\mathrm{Fin}\left(d\right)\to F))),\forall (a:F),\forall (b:F),(\mathrm{IsEquiangularSystem}\left(B,\phi ,a,b\right))\Rightarrow ((a^2\ne b)\Rightarrow (a^2=((d:F)+2)\cdot b)))))))$$

Formalization. D5/S3/QuadraticForms/GerzonEqualityParameterIdentity.claim (✓ std3).

Citation. Gary R. W. Greaves, Joseph W. Iverson, John Jasper, Dustin G. Mixon (2021). Frames over finite fields: Equiangular lines in orthogonal geometry. DOI: 10.48550/arXiv.2012.13642. URL: https://arxiv.org/abs/2012.13642v2.

Commentary.

Example 5.8, page 21: “The authors do not know how to construct an ETF with any of the parameters given in Table 4. In particular, every instance of Gerzon equality that we currently know satisfies the identity a² = (d + 2)b, but this equation does not occur anywhere in Table 4 (where b = 1). Proposition 2.10 implies that a² = (d + 2)b whenever Gerzon’s bound is saturated, d ≢ₚ 0, and d ≢ₚ 1. The authors do not know if these conditions can be removed.” Here F is finite, ringChar F differs from two, d is any natural number at least two, and B is symmetric and nondegenerate. The number of vectors is exactly Nat.choose (d + 1) 2, the Gerzon bound of Proposition 2.9. The inequality a² ≠ b is retained. Casting d into F precedes field addition and multiplication. There is no restriction on d modulo the characteristic. Proposition 2.10 supplies the earlier ETF parameter equation, while this statement asks for the identity without the two dimension congruences.

Theorem 1.5 (Gerzon equality fixes the parameters).

$$\mathrm{claim}$$

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

Resolves. Problems/greaves-iverson-jasper-mixon-2021-gerzon-equality-identity (proved) by D5/S3/QuadraticForms/GerzonEqualityParameterIdentity.result.

Source. Repository-derived.

Acknowledgement. Gary R. W. Greaves, Joseph W. Iverson, John Jasper, Dustin G. Mixon (2021). Frames over finite fields: Equiangular lines in orthogonal geometry. DOI: 10.48550/arXiv.2012.13642. URL: https://arxiv.org/abs/2012.13642v2.

Commentary.

The statement holds, including dimensions congruent to zero or one in the field. An orthogonal basis reduces the form to diagonal coordinates. The rank-one operators either form a basis of the selfadjoint-matrix space or span its trace-zero hyperplane. Their fourth-moment operator has the form α·id + β·tr·I; comparison of a diagonal matrix unit and a symmetric off-diagonal pair forces α = 2β. The resulting parameter equation uses no division by d or d − 1. The proof also works over infinite fields of characteristic different from two. Dimension one is excluded: with one vector the off-diagonal equation has no instances, so b can vary independently of a.

References

• Truth anchor: D5/S3/QuadraticForms/GerzonEqualityParameterIdentity.IsEquiangularSystem
• Truth anchor: D5/S3/QuadraticForms/GerzonEqualityParameterIdentity.claim
• Truth anchor: D5/S3/QuadraticForms/GerzonEqualityParameterIdentity.gram_pair_sum
• Truth anchor: D5/S3/QuadraticForms/GerzonEqualityParameterIdentity.independent_nonzero_trace
• Truth anchor: D5/S3/QuadraticForms/GerzonEqualityParameterIdentity.result