English
The root of a certain polynomial P_n determines the (n+1)-st coefficient in a recursive construction for Witt vectors; P_n encodes the defining relation of that coefficient.
Русский
Корень для данного многочлена P_n определяет (n+1)-й коэффициент в рекурсивном построении Witt-вектора; P_n кодирует задающее равенство для этого коэффициента.
LaTeX
$$succNthDefiningPoly(p,n,a1,a2,bs) ∈ Polynomial(k) and its root determines the (n+1)st coefficient in the recursive construction$$
Lean4
/-- The root of this polynomial determines the `n+1`st coefficient of our solution. -/
def succNthDefiningPoly (n : ℕ) (a₁ a₂ : 𝕎 k) (bs : Fin (n + 1) → k) : Polynomial k :=
X ^ p * C (a₁.coeff 0 ^ p ^ (n + 1)) - X * C (a₂.coeff 0 ^ p ^ (n + 1)) +
C
(a₁.coeff (n + 1) * (bs 0 ^ p) ^ p ^ (n + 1) + nthRemainder p n (fun v => bs v ^ p) (truncateFun (n + 1) a₁) -
a₂.coeff (n + 1) * bs 0 ^ p ^ (n + 1) -
nthRemainder p n bs (truncateFun (n + 1) a₂))
