Uniqueness of the CAR staircase occupation weight

The half-integral weights arising from the CAR model have the form a i + 1 / 2, where a is a tuple of natural-number occupation counts. This file specializes the integer staircase criterion from TauCeti.Combinatorics.Majorization to the finite natural-number tuples produced by that model.

Main results

• TauCeti.eq_finRev_of_antitone_of_prefix_sum_le_of_sum_eq_of_casimir_eq: a natural occupation tuple dominated by Fin.rev, with the same total and quadratic sum, is Fin.rev.

References

• D. Panyushev, The exterior algebra and "spin" of an orthogonal g-module, Transform. Groups 6 (2001), 371–396, Proposition 2.4 and Example 2.5(1), for the CAR staircase-weight application.

theorem TauCeti.eq_finRev_of_antitone_of_prefix_sum_le_of_sum_eq_of_casimir_eq {N : ℕ} (a : Fin N → ℕ) (ha : Antitone a) (hmajor : ∀ (k : ℕ) (hk : k < N), ∑ i : Fin k, ↑(a (Fin.castLE ⋯ i)) ≤ ∑ i : Fin k, ↑↑(Fin.castLE ⋯ i).rev) (hsum : ∑ i : Fin N, ↑(a i) = ∑ i : Fin N, ↑↑i.rev) (hcasimir : ∑ i : Fin N, ↑(a i) * (↑(a i) + ↑N - 2 * ↑↑i) = ∑ i : Fin N, ↑↑i.rev * (↑↑i.rev + ↑N - 2 * ↑↑i)) : a = fun (i : Fin N) => ↑i.rev

A majorized occupation weight with the staircase quadratic value is the staircase.

Let a : Fin N → ℕ be weakly decreasing. Suppose every proper initial sum of a is at most the corresponding initial sum of the reverse-index tuple i ↦ N - 1 - i, and suppose the total sums are equal. If the two tuples also have the same value under

a ↦ ∑ i, a i * (a i + N - 2i),

then a is the reverse-index tuple. For CAR highest weights this is the integral form of the trace-form gl_N Casimir polynomial after a common half-unit shift.