Sharp square dimension growth via the exponential bound

The sharp form of the square-dimension growth: it runs on the analytic n ^ n ≤ e ^ n · n ! (one term of the Taylor series of exp) where square_growth runs on the cruder combinatorial n ^ n ≤ 3 ^ n · n !, and it is the sharp constant that yields the displayed 2e of the paper.

theorem RS.square_growth_sharp (R : ℝ) (hR : 0 ≤ R) (s : ℕ) (hs : 2 * Real.exp 1 * 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₀)

Sharp square dimension growth. For a real R ≥ 0 and any s > 2eR, every submodule of the regular module whose character equals the JT character of the s × s square diagram has dimension exceeding R ^ (s²).

This recovers the paper's displayed 2e: the proof runs on n ^ n ≤ e ^ n · n !, and it is that e which appears in the threshold. The paper makes no claim that 2e cannot be improved.