2.5. Square roots🔗

A square root of a series is determined by its constant coefficient, as long as 2 times that coefficient is a unit. So the caller chooses a square root r of the constant coefficient, and supplies an inverse v of 2r:

Hex.TSeries.sqrtOfRoot.{u} {R : Type u} {n : ℕ} [Lean.Grind.CommRing R]
  (a : Hex.TSeries R n) (r v : R) : Hex.TSeries R n
Hex.TSeries.sqrtOfRoot.{u} {R : Type u}
  {n : ℕ} [Lean.Grind.CommRing R]
  (a : Hex.TSeries R n) (r v : R) :
  Hex.TSeries R n

Hex.TSeries.sqrtOfRoot_sq.{u} {R : Type u} {n : ℕ}
  [Lean.Grind.CommRing R] (a : Hex.TSeries R n) (r v : R)
  (hr : r * r = a.coeff 0) (hv : (1 + 1) * r * v = 1) :
  a.sqrtOfRoot r v * a.sqrtOfRoot r v = a
Hex.TSeries.sqrtOfRoot_sq.{u} {R : Type u}
  {n : ℕ} [Lean.Grind.CommRing R]
  (a : Hex.TSeries R n) (r v : R)
  (hr : r * r = a.coeff 0)
  (hv : (1 + 1) * r * v = 1) :
  a.sqrtOfRoot r v * a.sqrtOfRoot r v = a

Hex.TSeries.sqrt_unique.{u} {R : Type u} {n : ℕ} [Lean.Grind.CommRing R]
  (s t : Hex.TSeries R n) (r v : R) (hv : (1 + 1) * r * v = 1)
  (hs : s * s = t * t) (hsr : s.coeff 0 = r) (htr : t.coeff 0 = r) :
  s = t
Hex.TSeries.sqrt_unique.{u} {R : Type u}
  {n : ℕ} [Lean.Grind.CommRing R]
  (s t : Hex.TSeries R n) (r v : R)
  (hv : (1 + 1) * r * v = 1)
  (hs : s * s = t * t)
  (hsr : s.coeff 0 = r)
  (htr : t.coeff 0 = r) : s = t

The generating function c(x) = Σ Cₖ xᵏ of the Catalan numbers satisfies c = 1 + x c², so x c(x) = (1 - √(1 - 4x))/2, taking the square root with constant coefficient 1:

#v[0, 1, 1, 2, 5, 14, 42, 132, 429, 1430]

Neither half of the condition that 2r is a unit can be dropped. Over ℤ/2ℤ, where r = 1 is a unit but 2 is not, 1 + x has no square root at precision 2, since (1 + bx)² = 1 + b²x². Over ℤ/9ℤ, where 2 is a unit but r = 3 is not, x has no square root with constant coefficient 3 at precision 2, since (3 + bx)² = 6bx and 6b = 1 has no solution.

The square root is computed by Newton's method for the inverse square root z = 1/√a, with the step z ↦ z(3 - az²)/2, starting from 1/r; the result is az. This needs no inversion of a series at any step.

Hex.TSeries.sqrt? checks that r² = a₀ and, from precision 2 on, looks up the inverse of 2r with UnitOps. (At precision 1 the answer is the constant r, and at precision 0 there is nothing to check.) Over ℤ it fails on 1 - 4x, because 2 is not a unit of ℤ, even though the square root 1 - 2x - 2x² - 4x³ - ⋯ has integer coefficients:

none

The library never looks for r itself. Finding a square root in R is a question about R (over ℤ/pℤ for an odd prime p it is the Tonelli–Shanks algorithm), and the choice matters: when 2r is a unit in a nonzero ring, r and -r give different square roots. The Catalan numbers over ℤ come from the compositional inverse instead; see Composition and reversion.