29.2. Square roots and the golden ratio
Recall we construct integer polynomials using #p[a₀, a₁, …], i.e. giving its coefficients in increasing
degree, so #p[-2, 0, 1] is X² − 2. Its roots come back real first and in
increasing order, so index 1 is +√2:
open Hex
namespace HexNumberFieldChapter
def sqrt2 : AlgebraicNumber :=
(ZPoly.algebraicRoots #p[-2, 0, 1])[1]!
def sqrt3 : AlgebraicNumber :=
(ZPoly.algebraicRoots #p[-3, 0, 1])[1]!
#guard (ZPoly.algebraicRoots #p[-2, 0, 1]).size = 2
#guard sqrt2 * sqrt2 = 2
#guard (sqrt2 + sqrt3).p = #p[1, 0, -10, 0, 1]
#guard (sqrt2 + sqrt3)⁻¹ = sqrt3 - sqrt2
The field p of a canonical number is its minimal polynomial, so the third
check is the classical fact that √2 + √3 has minimal polynomial
X⁴ − 10X² + 1, and the fourth is 1 / (√2 + √3) = √3 − √2. Equality of
canonical numbers is decidable. Without the Mathlib companion, compare with
==, the executable test; with it, = is available too, because the
companion proves that the test is correct. A number prints as the
expression that rebuilds it: Hex.ZPoly.rootNear names the root of a polynomial
nearest to a point, and the printed point is the number's certified
approximation with enough digits that no other root is nearer:
#eval sqrt2 + sqrt3
So √2 + √3 can also be written as the root of its minimal polynomial near
3.146, and the imaginary unit as the root of X² + 1 near i:
#guard ZPoly.rootNear #p[1, 0, -10, 0, 1] 3.146 =
sqrt2 + sqrt3
#guard ZPoly.rootNear #p[1, 0, 1] 0 1 = AlgebraicNumber.I
A point equidistant from two roots resolves to the first in the output
order, so ZPoly.rootNear #p[-2, 0, 1] 0 is -√2.
The golden ratio is the positive root of X² − X − 1. Its defining identity,
its reciprocal, and the tenth Lucas number all fall out of decidable equality:
def φ : AlgebraicNumber :=
(ZPoly.algebraicRoots #p[-1, -1, 1])[1]!
#guard φ * φ = φ + 1
#guard φ⁻¹ = φ - 1
-- φ¹⁰ + φ⁻¹⁰ is the Lucas number L₁₀ = 123, so φ¹⁰ is a
-- root of X² − 123X + 1.
#guard (φ ^ (10 : Nat)).p = #p[1, -123, 1]