The trace-zeta theorem with the sharp threshold

The accompanying paper's Corollary A.2 in tower form, with the appendix's own hypothesis on dimensions and its own threshold: for a tower whose dimensions satisfy finrank (E n) ≤ A ^ n, and for every integer s > 2e√A, the trace zeta function of every element is P/Q with P and Q coprime, of constant term 1, and of degree at most s − 1 (traceZeta_rational_sharp); equivalently the power traces are a difference of power sums of two disjoint multisets of nonzero complex numbers of sizes at most s − 1 (traceZeta_superSpectrum_sharp).

The appendix begins with a rigid symmetric ℂ-linear category and an object Z, and derives the symmetric-group action on Z ^ ⊗ n, the propagation of vanishing, the traces and the Frobenius identity from the trace calculus. A FrobeniusTower assumes exactly those as an interface, and ObjectTower.lean constructs one from an arbitrary category-and-object pair, so traceZeta_rational_of_object is Corollary A.2 in the appendix's own generality; the skein endomorphism algebras instantiate the interface directly (SkeinTower.lean, BlockAssembly.lean).

TraceZeta.lean proves the same conclusions over an arbitrary Schur package with the side existentially quantified. The sharpness is in the quantifier and the constant: every admissible side gives its own degree bound, and the threshold is stated in the growth constant itself.

theorem RS.FrobeniusTower.traceZeta_rational_sharp {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 schurPackage E A Alg) (g : Alg) {s : ℕ} (hs : 2 * Real.exp 1 * √A < ↑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 (the accompanying paper, Corollary A.2, in tower form). For a tower whose dimensions are bounded by A ^ n, and for every integer s > 2e√A, the trace zeta function of every element of the ambient algebra is rational, ζ · Q = P, with P and Q coprime polynomials of constant term 1 and degree at most s − 1.

theorem RS.FrobeniusTower.traceZeta_superSpectrum_sharp {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 schurPackage E A Alg) (g : Alg) {s : ℕ} (hs : 2 * Real.exp 1 * √A < ↑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 form of Corollary A.2: for every integer s > 2e√A the power traces are a difference of power sums of two disjoint multisets of nonzero complex numbers, each of size at most s − 1.