数值半群的费尔共轭关系 conjectures

设 $S=\langle d_1,\dots,d_m\rangle$ 为数值半群，$k[S]$ 为其半环。$k[S]$ 的 Hilbert numerator 决定了归一化交替共轭幂和 $K_p(S)$，编码了共轭度的交替幂和。费尔 conjectured 给出 $K_p(S)$ 的显式公式，涉及间隙幂和 $G_r(S)=\sum_{g\notin S} g^r$ 以及普遍对称多项式 $T_n$ 在生成器幂和 $\sigma_k=\sum_i d_i^k$（以及 $\delta_k=(\sigma_k-1)/2^k$）处的评估。我们通过指数生成函数和系数提取证明了费尔 conjecture，isolating 所需的 $T_n$ 普遍恒等式。论文在 Lean/Mathlib 中完全形式化，且由 AxiomProver 从自然语言 conjecture 语句自动生成。