Sharp hook confinement

Hook confinement with the displayed constant of the accompanying paper, and with the threshold quantified as the appendix states it: relative to the assembled Schur package, every side s > 2e√A confines, not merely some side.

HookConfinement.lean proves the existential form over an arbitrary package. The constant here comes from the block dimensions of the assembled package, through square_growth_sharp.

theorem RS.schurPackage_dim (μ : YoungDiagram) : schurPackage.dim μ = nDim (jtSimple μ)

The assembled package's dimension field is the native block dimension of the chosen simple submodule.

theorem RS.PermTower.not_alive_square_sharp {E : ℕ → Type u} [(n : ℕ) → Ring (E n)] [(n : ℕ) → Algebra ℂ (E n)] {A : ℝ} [∀ (n : ℕ), Module.Finite ℂ (E n)] (T : PermTower E A) {s : ℕ} (hs : 2 * Real.exp 1 * √A < ↑s) : ¬T.Alive schurPackage (squareDiagram s)

Sharp square death: in a tower of growth A, the square of any side s > 2e√A is dead relative to the assembled package. Its block dimension exceeds √A ^ (s²) by square_growth_sharp, so the square of that dimension exceeds A ^ (s²), which is what not_alive_square asks for.

theorem RS.PermTower.hook_confinement_sharp {E : ℕ → Type u} [(n : ℕ) → Ring (E n)] [(n : ℕ) → Algebra ℂ (E n)] {A : ℝ} [∀ (n : ℕ), Module.Finite ℂ (E n)] (T : PermTower E A) {s : ℕ} (hs : 2 * Real.exp 1 * √A < ↑s) (μ : YoungDiagram) : T.Alive schurPackage μ → IsInHook (s - 1) (s - 1) μ

Sharp hook confinement: in a tower of growth A, every alive shape lies in the (s − 1, s − 1) hook, for every side s > 2e√A.