Polynomial calculus degree of the onto functional pigeonhole principle when the characteristic divides the surplus

The onto functional pigeonhole principle with $n+k$ pigeons and $n$ holes has a polynomialcalculus refutation of degree $1$ over $\mathbb F_p$ when $p\nmid k$, and one of degree$p^{v_p(k)}$ in general, by a criterion of Riis. We study the lower bound when $p$ divides$k$. In Lean~4 we prove that the degree is exactly $p$ when $p$ divides $k$ exactly once($n\ge2p-3$), at least $p+1$ when $p^2$ divides $k$ ($n\ge2p-1$), and at least $5$ for $p=2$,$k=8$ ($n\ge7$). With written proofs that rest on named published theorems and have beenchecked by AI reviewers but not by people, we show that the degree is exactly $p^{v_p(k)}$for $n\ge2p^{v_p(k)}-1$, so that for surplus $p^\ell$ it grows as $p^\ell$; we give twofurther mechanisms, one through Nullstellensatz designs (degree at least $2^\ell$ withexplicit thresholds) and one degree by degree (exact degree $p^2$ when $v_p(k)=2$); and werecord five errata in two of the sources these proofs use, among them a gap in the publishedproof of a theorem we would otherwise have used. Every statement carries itsevidence tier. All results were produced by AI research agents under the author's direction.