Thakur's hypotheses on power sums of ${\mathbb{F}}_q[t]$

In his 2009 paper, Thakur posed three conjectural hypotheses for the degrees of the power sums $$S_d(k)=\sum _{\begin{array}{c}a\in {\mathbb{F}}_q[t]\text{ monic}\\ \mathrm{°}a=d\end{array}}{a}^{-k}\text{and}{s}_d(k)=-{\mathrm{°}}_t{S}_d(k)\mathrm{.}$$ For prime fields $q=p$, we prove Hypotheses H1 and H2, giving a unique greedy description of the extremal term in Carlitz’s formula and establishing the recursion $$s_d(k)=s_{d-1}(s_1(k))+s_1(k)\mathrm{.}$$ As consequences, the prime-field recursion gives the strict Newton-polygon convexity used in the prime-field Carlitz-Goss Riemann-hypothesis theorem, and it recovers Thakur’s nonvanishing theorem for positive multizeta values over ${\mathbb{F}}_p[t]$. We also prove Hypothesis H3 for all finite fields $q=p^f$, establishing the monotonicity $$s_d(k)<s_d(k+1)(p\nmid k)\mathrm{.}$$ We provide Lean formalizations of the arguments in this paper, generated by AxiomProver.