def Hex.TSeries.sqrtStep {R : Type u} {n : Nat} [Lean.Grind.CommRing R] (a : TSeries R n) (halfInv : R) (z : TSeries R n) (m : Nat) : TSeries R n

One bounded inverse-square-root Newton update.

Equations

• a.sqrtStep halfInv z m = Hex.TSeries.mulUpTo m (Hex.TSeries.mulUpTo m z (Hex.TSeries.C (1 + 1 + 1) - Hex.TSeries.mulUpTo m a (Hex.TSeries.mulUpTo m z z))) (Hex.TSeries.C halfInv)

def Hex.TSeries.sqrtUpTo {R : Type u} {n : Nat} [Lean.Grind.CommRing R] (m : Nat) (a : TSeries R n) (r v : R) : TSeries R n

Lift the supplied root through a bounded precision.

Equations

• One or more equations did not get rendered due to their size.

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

The square root of a above r, given a witness inverting 2*r.

Equations

• a.sqrtOfRoot r v = Hex.TSeries.sqrtUpTo n a r v

def Hex.TSeries.sqrt? {R : Type u} {n : Nat} [Lean.Grind.CommRing R] [DecidableEq R] [UnitOps R] (a : TSeries R n) (r : R) : Option (TSeries R n)

Check the supplied constant root and look up the inverse needed to lift it.

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.TSeries.sqrtUpTo_agree {R : Type u} {n : Nat} [Lean.Grind.CommRing R] (m : Nat) (a : TSeries R n) (r v : R) (hr : r * r = a.coeff 0) (hv : (1 + 1) * r * v = 1) : Agree m (sqrtUpTo m a r v) (a.sqrtOfRoot r v)

Bounded square-root lifting agrees with the full lift throughout the requested prefix.

theorem Hex.TSeries.sqrtOfRoot_sq {R : Type u} {n : Nat} [Lean.Grind.CommRing R] (a : 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

Newton lifting squares to the input under the stated root and unit hypotheses.

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

The lifted square root retains the chosen constant root.

theorem Hex.TSeries.sqrt_unique {R : Type u} {n : Nat} [Lean.Grind.CommRing R] (s t : 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

A square root is unique once its constant root has been fixed and 2*r is a unit.

theorem Hex.TSeries.sqrt?_isSome_iff {R : Type u} {n : Nat} [Lean.Grind.CommRing R] [DecidableEq R] [UnitOps R] [LawfulUnitOps R] (a : TSeries R n) (r : R) : (a.sqrt? r).isSome = true ↔ n = 0 ∨ r * r = a.coeff 0 ∧ (n ≤ 1 ∨ ∃ (v : R), (1 + 1) * r * v = 1)

Optional square-root lifting has the precision-sensitive success condition required by the zero and one coefficient cases.