The quantitative trace-zeta theorem

In a Frobenius tower, the trace zeta function of every element is rational with numerator and denominator degrees bounded by the hook parameter. This combines hook confinement (dead shapes outside a hook) with the Frobenius identity (turning dead shapes into Schur vanishing) and the rationality and reduced super-spectrum results from ZetaRational and HookVanishing.

The side is existentially quantified here, and the package is arbitrary. TraceZetaSharp.lean states the same conclusions in the appendix's own generality: a real dimension bound and every side above 2e√A.

Unlike NilpotentTrace, no nilpotency hypothesis is needed: the hook-vanishing half of the proof uses only the Frobenius identity and hook confinement, both of which hold for every element.

theorem RS.FrobeniusTower.traceZeta_rational {P : SchurPackage} {E : ℕ → Type u} [(n : ℕ) → Ring (E n)] [(n : ℕ) → Algebra ℂ (E n)] {A : ℝ} {Alg : Type u} [Ring Alg] [Algebra ℂ Alg] [∀ (n : ℕ), Module.Finite ℂ (E n)] (T : FrobeniusTower P E A Alg) (g : Alg) : ∃ (s : ℕ) (Pp : Polynomial ℂ) (Qp : Polynomial ℂ), Pp.coeff 0 = 1 ∧ Qp.coeff 0 = 1 ∧ Pp.natDegree ≤ s - 1 ∧ Qp.natDegree ≤ s - 1 ∧ IsCoprime Pp Qp ∧ (traceZeta fun (m : ℕ) => T.traceA (g ^ m)) * ↑Qp = ↑Pp

The trace-zeta theorem over an arbitrary Schur package: in a Frobenius tower, the trace zeta function of every element is rational with numerator and denominator degrees bounded by the hook parameter the package's growth field supplies. Corollary A.2 of the accompanying paper, with its real growth constant and its threshold on every side, is traceZeta_rational_sharp in TraceZetaSharp.lean.

theorem RS.FrobeniusTower.traceZeta_superSpectrum {P : SchurPackage} {E : ℕ → Type u} [(n : ℕ) → Ring (E n)] [(n : ℕ) → Algebra ℂ (E n)] {A : ℝ} {Alg : Type u} [Ring Alg] [Algebra ℂ Alg] [∀ (n : ℕ), Module.Finite ℂ (E n)] (T : FrobeniusTower P E A Alg) (g : Alg) : ∃ (s : ℕ) (alpha : Multiset ℂ) (beta : Multiset ℂ), alpha.card ≤ s - 1 ∧ beta.card ≤ s - 1 ∧ (∀ x ∈ alpha, x ≠ 0) ∧ (∀ x ∈ beta, x ≠ 0) ∧ (∀ x ∈ alpha, x ∉ beta) ∧ ∀ (m : ℕ), 1 ≤ m → T.traceA (g ^ m) = (Multiset.map (fun (x : ℂ) => x ^ m) alpha).sum - (Multiset.map (fun (x : ℂ) => x ^ m) beta).sum

The reduced super-spectrum corollary: the trace sequence of every element in a Frobenius tower is a difference of power sums of two disjoint multisets of nonzero complex numbers of sizes at most s − 1.