theorem Hex.AlgebraicNumber.Radical.principalSide_value (a : AlgebraicNumber) {n : ℕ} (hn : 1 < n) (ha : a.toComplex ≠ 0) : (if (a.toComplex ^ (↑n)⁻¹).im = 0 then RootSide.real else if 0 < (a.toComplex ^ (↑n)⁻¹).im then RootSide.upper else RootSide.lower) = principalSide a

The exact side of the principal radical for a nonzero input and index at least two.

theorem Hex.AlgebraicNumber.Radical.fast?_sound (a : AlgebraicNumber) {n : ℕ} (hn : 1 < n) (ha : a.toComplex ≠ 0) (roots : Array RootCount) (hroots : ∀ r ∈ roots.toList, r.root.toComplex ^ n = a.toComplex) (hprincipal : ∃ r ∈ roots.toList, r.root.toComplex = a.toComplex ^ (↑n)⁻¹) {out : AlgebraicRoot} (h : fast? a roots = some out) : out.toComplex = a.toComplex ^ (↑n)⁻¹

A successful lazy branch selection is the principal root of the input.