The factorial obstruction to a nonzero nilpotent trace

Schrijver's argument (arXiv:1211.3561, Proposition 4) uses only permutation representations and the cycle-trace identity. A last nonzero power trace separates all permutations, forcing dimension at least n! at every level. A single level of smaller dimension therefore suffices for nilpotent-trace vanishing.

CycleTraceTower records precisely these inputs, without Schur idempotents, branching, hook confinement or rationality. The object and strand instances are supplied in Novel/Envelope/FactorialTrace and Novel/Envelope/BlockFactorialTrace.

structure RS.CycleTraceTower (E : ℕ → Type u_1) [(n : ℕ) → Ring (E n)] [(n : ℕ) → Algebra ℂ (E n)] (A : Type u_2) [Ring A] [Algebra ℂ A] : Type (max u_1 u_2)

Permutation representations and tensor-power traces satisfying the cycle formula, with fixed points recorded separately.

• traceA : A →ₗ[ℂ] ℂ

  The trace on the ambient algebra.

• trace (n : ℕ) : E n →ₗ[ℂ] ℂ

  The trace at each tensor level.

• rep (n : ℕ) : Equiv.Perm (Fin n) →* E n

  The permutation representations.

• pow (n : ℕ) : A → E n

  The tensor-power maps; their cycle traces are all that is used.

• cycleTrace (n : ℕ) (π : Equiv.Perm (Fin n)) (g : A) : (self.trace n) ((self.rep n) π * self.pow n g) = (Multiset.map (fun (c : ℕ) => self.traceA (g ^ c)) π.cycleType).prod * self.traceA g ^ (n - π.cycleType.sum)

  The trace of a permutation against a tensor power is the product of the traces along its cycles.

theorem RS.CycleTraceTower.trace_perm_pow {E : ℕ → Type u_1} [(n : ℕ) → Ring (E n)] [(n : ℕ) → Algebra ℂ (E n)] {A : Type u_2} [Ring A] [Algebra ℂ A] (T : CycleTraceTower E A) {y : A} (hy : SinglePowerTrace T.traceA y) (n : ℕ) (π : Equiv.Perm (Fin n)) : (T.trace n) ((T.rep n) π * T.pow n y) = if π = 1 then T.traceA y ^ n else 0

For an isolated nonzero power trace, every nonidentity permutation has zero trace against the tensor power.

theorem RS.CycleTraceTower.linearIndependent_rep {E : ℕ → Type u_1} [(n : ℕ) → Ring (E n)] [(n : ℕ) → Algebra ℂ (E n)] {A : Type u_2} [Ring A] [Algebra ℂ A] (T : CycleTraceTower E A) {y : A} (hy : SinglePowerTrace T.traceA y) (n : ℕ) : LinearIndependent ℂ fun (π : Equiv.Perm (Fin n)) => (T.rep n) π

An isolated nonzero power trace makes all permutation operators linearly independent.

theorem RS.CycleTraceTower.factorial_le_finrank {E : ℕ → Type u_1} [(n : ℕ) → Ring (E n)] [(n : ℕ) → Algebra ℂ (E n)] {A : Type u_2} [Ring A] [Algebra ℂ A] (T : CycleTraceTower E A) {g : A} (hg : IsNilpotent g) (hτ : T.traceA g ≠ 0) (n : ℕ) [Module.Finite ℂ (E n)] : n.factorial ≤ Module.finrank ℂ (E n)

A nilpotent with nonzero trace forces factorial dimension at every finite-dimensional level.

theorem RS.CycleTraceTower.traceA_eq_zero_of_finrank_lt_factorial {E : ℕ → Type u_1} [(n : ℕ) → Ring (E n)] [(n : ℕ) → Algebra ℂ (E n)] {A : Type u_2} [Ring A] [Algebra ℂ A] (T : CycleTraceTower E A) {n : ℕ} [Module.Finite ℂ (E n)] (hbound : Module.finrank ℂ (E n) < n.factorial) {g : A} (hg : IsNilpotent g) : T.traceA g = 0

One finite-dimensional level below factorial growth forces the trace of every nilpotent to vanish.

theorem RS.CycleTraceTower.traceA_eq_zero_of_exponential_bound {E : ℕ → Type u_1} [(n : ℕ) → Ring (E n)] [(n : ℕ) → Algebra ℂ (E n)] {A : Type u_2} [Ring A] [Algebra ℂ A] (T : CycleTraceTower E A) [∀ (n : ℕ), Module.Finite ℂ (E n)] (B : ℝ) (hbound : ∀ (n : ℕ), ↑(Module.finrank ℂ (E n)) ≤ B ^ n) {g : A} (hg : IsNilpotent g) : T.traceA g = 0

Exponential endomorphism growth is a sufficient instance of the single-level factorial bound.