Papers With

← All papers
First page of Polynomiality of the Generalized Verschiebung Degree

Polynomiality of the Generalized Verschiebung Degree

Siqing Zhang

math.AG Jun 24, 2026 · v1 math.CO
formalization combinatorics algebra
Read PDF arXiv abstract Code
TL;DR
The combinatorial core results (Lemma 7, Theorem 2, Lemma 10) were formalized and verified in Lean 4, with a cited artifact.
Abstract
For a general curve in positive characteristic, taking the Frobenius pullback induces a generically finite rational map V on the moduli space of rank 2 vector bundles with trivial determinant. Recently, Kondo–Wakabayashi show that the generic degree of V, considered as a function on the characteristic of the base field, is a quasi-polynomial. In this paper, we show that this quasi-polynomial is indeed a polynomial, and we write out this polynomial explicitly.
Problem

Kondo–Wakabayashi showed that the generic degree of the generalized Verschiebung on the moduli of rank 2 trivial-determinant bundles over a general curve in characteristic p is a quasi-polynomial in p. The open question was whether it is a genuine polynomial for every genus.

Approach

The paper proves a bijection between sets of edge-numberings on trivalent graphs, Ed_{P,N,G} ≅ Ed_{P,1,G} × Ed_{2P,1,G}^{N-1}, which reduces deg(V) to |Ed_{2p,1,G}|. This count is written as the trace of a power of a transfer matrix. The matrix is diagonalized using trigonometric sums, yielding explicit csc-sum formulas. The combinatorial lemmas behind these steps were formalized in Lean 4.

Results

For all genus g ≥ 2, deg(V) = p^{g-1} R_g(p^2), where R_g is an explicit polynomial expressed through Bernoulli numbers and Laurent coefficients of csc^{2g-2}. The quasi-polynomial is therefore always a polynomial.