The square dimension growth #
Evaluating the natural dimension identity at square diagrams: the
Vandermonde side is the superfactorial, the factorial side is at
most (2s)^(s²) times it, so the dimension dominates
(s²)^(s²) / (6s)^(s²) = (s/6)^(s²) — beating any R^(s²) for
s = 6(R+1). The factorial lower bound n^n ≤ 3^n·n! enters as
the hypothesis H3, discharged in FactorialBound.lean.
theorem
RS.square_V_eq
(s : ℕ)
:
∏ i : Fin (squareDiagram s).rowLens.length,
∏ j > i, (eStair (squareDiagram s) (Fin.revPerm j) - eStair (squareDiagram s) (Fin.revPerm i)) = ∏ i : Fin (squareDiagram s).rowLens.length, ((squareDiagram s).rowLens.length - 1 - ↑i).factorial
The square Vandermonde side is the superfactorial.
The square factorial side is bounded by (2s)^(s²) times the
superfactorial.
theorem
RS.square_growth
(H3 : ∀ (n : ℕ), n ^ n ≤ 3 ^ n * n.factorial)
(R : ℕ)
:
∃ (s : ℕ),
∀
(S₀ :
Submodule (MonoidAlgebra ℂ (Equiv.Perm (Fin (squareDiagram s).card)))
(MonoidAlgebra ℂ (Equiv.Perm (Fin (squareDiagram s).card)))),
(∀ (π : Equiv.Perm (Fin (squareDiagram s).card)), jtChar (squareDiagram s) π = nChar S₀ π) → R ^ s ^ 2 < nDim S₀
The square dimension growth, modulo the factorial lower bound.