The coordinate spectrum of CAR diagonal eigenvectors

For the left regular action of gl_n on the Clifford algebra of its trace form, every eigenvalue of a diagonal matrix unit on a nonzero vector is one of the half-integral expressions m + 1/2 for a natural number m < n. In particular, this restricts every coordinate of a highest weight.

The diagonal lift is a sum of commuting occupation projections together with its scalar diagonal term. Removing the diagonal 1/2 from a diagonal eigenvector equation leaves n - 1 commuting idempotents, reducing the coordinate result to the general spectrum theorem for their sum.

More generally, summing diagonal equations over a subset s leaves the commuting occupation projections crossing from s to its complement. Their eigenvalue is a natural number m bounded by |s| (n - |s|). Consequently, natural occupation counts for the coordinates have subset sum choose |s| 2 + m. This gives all cut bounds at once, while the full subset has no crossing terms and fixes the total sum.

Main results

• TauCeti.exists_eq_natCast_add_inv_two_of_lie_single_self_eq_smul: every diagonal matrix-unit eigenvalue has the form m + 1/2 with m < n.
• TauCeti.IsGlHighestWeightVector.exists_weight_apply_eq_natCast_add_inv_two: every coordinate of a CAR highest weight has the form m + 1/2 with m < n.
• TauCeti.exists_sum_eq_choose_two_add_of_lie_single_self_eq_smul: occupation counts on a subset have the form choose |s| 2 + m, with m bounded by the size of the cut.
• TauCeti.exists_sum_eq_natCast_add_card_sq_div_two_of_lie_single_self_eq_smul: without a CharZero assumption, but with two invertible, the sum of the diagonal eigenvalues is a bounded natural cast plus |s|² / 2.

References

• D. Panyushev, The exterior algebra and "spin" of an orthogonal g-module, Transformation Groups 6 (2001), 371–396, Proposition 2.4 and Example 2.5(1).
• D. Shlyakhtenko, Failure of Strong Convergence of Matrices with Fermionic Entries, arXiv:2606.28648, §2.3.

theorem TauCeti.exists_sum_eq_natCast_add_card_sq_div_two_of_lie_single_self_eq_smul {K : Type u_1} {n : Type u_2} [Field K] [Fintype n] [h2 : Invertible 2] [decEq : DecidableEq n] {μ : n → K} {v : CliffordAlgebra (traceQuadraticForm K n)} (s : Finset n) (hv : v ≠ 0) (hdiag : ∀ i ∈ s, ⁅Matrix.single i i 1, v⁆ = μ i • v) : ∃ m ≤ s.card * (Fintype.card n - s.card), ∑ i ∈ s, μ i = ↑m + ↑s.card ^ 2 / 2

If a nonzero vector is a simultaneous eigenvector for the diagonal matrix units indexed by s, the sum of their eigenvalues is m + |s|² / 2, where m is a natural number bounded by the number of ordered pairs crossing from s to its complement.

The natural number is the eigenvalue of the sum of the commuting cut occupation projections. No CharZero, finite-dimensionality, or splitting hypothesis is needed, but two must be invertible.

theorem TauCeti.exists_eq_natCast_add_inv_two_of_lie_single_self_eq_smul {K : Type u_1} {n : Type u_2} [Field K] [Fintype n] [h2 : Invertible 2] [decEq : DecidableEq n] {μ : K} {v : CliffordAlgebra (traceQuadraticForm K n)} {i : n} (hv : v ≠ 0) (hdiag : ⁅Matrix.single i i 1, v⁆ = μ • v) : ∃ m < Fintype.card n, μ = ↑m + 2⁻¹

Every eigenvalue of a diagonal matrix unit on a nonzero vector in the left regular CAR module is a natural number less than the matrix size, shifted by 1/2.

theorem TauCeti.exists_sum_eq_choose_two_add_of_lie_single_self_eq_smul {K : Type u_1} {n : Type u_2} [Field K] [Fintype n] [h2 : Invertible 2] [decEq : DecidableEq n] [CharZero K] {μ : n → K} {a : n → ℕ} {v : CliffordAlgebra (traceQuadraticForm K n)} (s : Finset n) (hv : v ≠ 0) (hdiag : ∀ i ∈ s, ⁅Matrix.single i i 1, v⁆ = μ i • v) (hμ : ∀ i ∈ s, μ i = ↑(a i) + 2⁻¹) : ∃ m ≤ s.card * (Fintype.card n - s.card), ∑ i ∈ s, a i = s.card.choose 2 + m

Let a nonzero vector be a simultaneous eigenvector for the diagonal matrix units, with each eigenvalue written as a natural occupation count plus 1/2. On a subset s, the sum of the counts is choose |s| 2 + m, where m is bounded by the number of ordered pairs crossing from s to its complement.

The natural number m is the eigenvalue of the sum of the commuting cut occupation projections. No finite-dimensionality or splitting hypothesis is needed.

theorem TauCeti.sum_le_choose_two_add_card_mul_sub_of_lie_single_self_eq_smul {K : Type u_1} {n : Type u_2} [Field K] [Fintype n] [h2 : Invertible 2] [decEq : DecidableEq n] [CharZero K] {μ : n → K} {a : n → ℕ} {v : CliffordAlgebra (traceQuadraticForm K n)} (s : Finset n) (hv : v ≠ 0) (hdiag : ∀ i ∈ s, ⁅Matrix.single i i 1, v⁆ = μ i • v) (hμ : ∀ i ∈ s, μ i = ↑(a i) + 2⁻¹) : ∑ i ∈ s, a i ≤ s.card.choose 2 + s.card * (Fintype.card n - s.card)

Under the hypotheses of TauCeti.exists_sum_eq_choose_two_add_of_lie_single_self_eq_smul, the occupation-count sum on s is bounded by choose |s| 2 + |s| (n - |s|).

theorem TauCeti.sum_univ_eq_choose_two_of_lie_single_self_eq_smul {K : Type u_1} {n : Type u_2} [Field K] [Fintype n] [h2 : Invertible 2] [decEq : DecidableEq n] [CharZero K] {μ : n → K} {a : n → ℕ} {v : CliffordAlgebra (traceQuadraticForm K n)} (hv : v ≠ 0) (hdiag : ∀ (i : n), ⁅Matrix.single i i 1, v⁆ = μ i • v) (hμ : ∀ (i : n), μ i = ↑(a i) + 2⁻¹) : ∑ i : n, a i = (Fintype.card n).choose 2

For simultaneous half-shifted natural diagonal eigenvalues, the total occupation count is choose n 2. This is the full-subset case of the cut calculation, where no projection crosses the boundary.

theorem TauCeti.IsGlHighestWeightVector.exists_weight_apply_eq_natCast_add_inv_two {K : Type u_1} {n : Type u_2} [Field K] [Fintype n] [h2 : Invertible 2] [LinearOrder n] [DecidableEq n] {μ : n → K} {v : CliffordAlgebra (traceQuadraticForm K n)} (hv : IsGlHighestWeightVector μ v) (i : n) : ∃ m < Fintype.card n, μ i = ↑m + 2⁻¹

Every coordinate of a highest weight in the left regular CAR module is a natural number less than the matrix size, shifted by 1/2.

This statement supplies the coordinate restriction; it does not assert that every expression is attained by a given vector.