The counting form of the double-sum identity #
Substituting the tuple-count coefficients and the guard/margin
bridges into the signed double-sum identity: the signed count of
margin-constrained Sym-tuples over shifted compositions is 1.
theorem
RS.t_count
{k : ℕ}
(v : Fin k → ℕ)
(hsort : ∀ (i j : Fin k), i ≤ j → v j ≤ v i)
:
(∑ τ : Equiv.Perm (Fin k),
∑ σ : Equiv.Perm (Fin k),
↑↑(Equiv.Perm.sign τ) * ↑↑(Equiv.Perm.sign σ) * if (∀ (i : Fin k), 0 ≤ ↑(v i) + ↑↑(σ i) - ↑↑i) ∧ ∀ (i : Fin k), 0 ≤ ↑(v i) + ↑↑(τ i) - ↑↑i then
↑(Fintype.card
{ W : (i : Fin k) → Sym (Fin k) (↑(v i) + ↑↑(σ i) - ↑↑i).toNat // ∀ (j : Fin k), ∑ i : Fin k, Multiset.count j ↑(W i) = (↑(v j) + ↑↑(τ j) - ↑↑j).toNat })
else 0) = 1
The counting form of the double-sum identity.