The two halves of the dimension bound

The tower half is unconditional: at any side s > 2eR the skein representation kills the square block idempotent (skeinRep_square_dead). The model half is parameterized -- any linear map out of the group algebra that factors the kill and admits a trace functional with plain or signed constant-cycle-product character forces the constant below s (sector_bound_of_dead, sector_bound_of_dead_signed), provided the square Schur value at that constant is nonzero.

The two are composed in Interfaces/SectorDischarge.lean, against the sector traces of SectorIntertwine.lean and the binomial determinant of SymFun/LGVStrict.lean.

theorem RS.jtSimple_dim_pos (μ : YoungDiagram) : 0 < nDim (jtSimple μ)

The chosen block dimension is positive.

theorem RS.skeinRep_square_dead {R : ℕ} (f : EdgeRankParameter R) {s : ℕ} (hs : 2 * Real.exp 1 * ↑R < ↑s) : (skeinRep f (squareDiagram s).card) (charIdempotent (nDim (jtSimple (squareDiagram s))) (jtChar (squareDiagram s))) = 0

Square death in the skein tower: at any side s > 2eR the skein representation kills the square block idempotent.

theorem RS.sector_bound_of_dead {s m : ℕ} {M : Type u_1} [AddCommGroup M] [Module ℂ M] (ρ : SymGroupAlgebra (squareDiagram s).card →ₗ[ℂ] M) (tr : M →ₗ[ℂ] ℂ) (htr : ∀ (π : Equiv.Perm (Fin (squareDiagram s).card)), tr (ρ ((MonoidAlgebra.of ℂ (Equiv.Perm (Fin (squareDiagram s).card))) π)) = cycleProd (fun (x : ℕ) => ↑m) π) (hSchur : s ≤ m → (diagramSchur (squareDiagram s) fun (x : ℕ) => ↑m) ≠ 0) (h0 : ρ (charIdempotent (nDim (jtSimple (squareDiagram s))) (jtChar (squareDiagram s))) = 0) : m < s

The even sector bound: a linear map with plain constant-cycle-product character that kills the square idempotent forces the constant below the side, given the Schur nonvanishing.

theorem RS.sector_bound_of_dead_signed {s m : ℕ} {M : Type u_1} [AddCommGroup M] [Module ℂ M] (ρ : SymGroupAlgebra (squareDiagram s).card →ₗ[ℂ] M) (tr : M →ₗ[ℂ] ℂ) (htr : ∀ (π : Equiv.Perm (Fin (squareDiagram s).card)), tr (ρ ((MonoidAlgebra.of ℂ (Equiv.Perm (Fin (squareDiagram s).card))) π)) = ↑↑(Equiv.Perm.sign π) * cycleProd (fun (x : ℕ) => ↑m) π) (hSchur : s ≤ m → (diagramSchur (squareDiagram s) fun (x : ℕ) => -↑m) ≠ 0) (h0 : ρ (charIdempotent (nDim (jtSimple (squareDiagram s))) (jtChar (squareDiagram s))) = 0) : m < s

The odd sector bound: the sign-twisted analogue, with the Schur nonvanishing at the negated constant.