x³ - x - 1, whose real root is the smallest Pisot number.
9.3. Worked example: the smallest Pisot number
Take p(x) = x³ − x − 1. It has one real root, the plastic constant
β ≈ 1.3247, and a complex-conjugate pair. Classically β is the smallest
Pisot number: a real algebraic integer greater than one all of whose other
conjugates lie strictly inside the unit disc. The companion does not formalize
that global minimality, or β's algebraic integrality; it certifies, for this
one polynomial, that the real root is pinned to eight decimal places and that
both other roots have norm below one, which is the Pisot condition for β.
def
The polynomial has only simple roots, so it meets Hex.isolate's precondition. The
companion proves this once, from a Bézout identity for p and p', and
reusing that lemma discharges the precondition:
open Hex HexRootsMathlib.Examples
example : HasOnlySimpleRoots pisot := pisot_simple
Running the driver, here with the Newton-Kantorovich strategy, to 32 bits
returns three atoms, and the companion identifies their semantic roots with the
three complex roots of x³ − x − 1:
theorem
HexRootsMathlib.Examples.isolate_pisot : ∃ atoms, Hex.isolate HexRootsMathlib.Examples.pisot HexRootsMathlib.Examples.pisot_simple 32 Hex.AtomStrategy.nk = some atoms ∧ atoms.size = 3 ∧ (List.map HexRootsMathlib.DyadicRootIsolation.root atoms.toList).toFinset = {HexRootsMathlib.Examples.pisotRealRoot, HexRootsMathlib.Examples.pisotLowerRoot, HexRootsMathlib.Examples.pisotUpperRoot} ∧ ∀ iso ∈ atoms.toList, 32 ≤ iso.square.precHexRootsMathlib.Examples.isolate_pisot : ∃ atoms, Hex.isolate HexRootsMathlib.Examples.pisot HexRootsMathlib.Examples.pisot_simple 32 Hex.AtomStrategy.nk = some atoms ∧ atoms.size = 3 ∧ (List.map HexRootsMathlib.DyadicRootIsolation.root atoms.toList).toFinset = {HexRootsMathlib.Examples.pisotRealRoot, HexRootsMathlib.Examples.pisotLowerRoot, HexRootsMathlib.Examples.pisotUpperRoot} ∧ ∀ iso ∈ atoms.toList, 32 ≤ iso.square.prec
The full driver succeeds, returns three atoms, and its semantic roots are the three explicitly bounded roots above.
The certificates pin the real root to eight decimal places and place both nonreal roots strictly inside the unit disc, which is the Pisot property stated for this polynomial:
theorem
HexRootsMathlib.Examples.pisot_property : 132471795 / 100000000 < HexRootsMathlib.Examples.pisotRealRoot.re ∧ HexRootsMathlib.Examples.pisotRealRoot.re < 132471796 / 100000000 ∧ HexRootsMathlib.Examples.pisotRealRoot.im = 0 ∧ ∀ z ∈ (HexRootsMathlib.toPolyℂ HexRootsMathlib.Examples.pisot).roots.toFinset, z ≠ HexRootsMathlib.Examples.pisotRealRoot → ‖z‖ < 1HexRootsMathlib.Examples.pisot_property : 132471795 / 100000000 < HexRootsMathlib.Examples.pisotRealRoot.re ∧ HexRootsMathlib.Examples.pisotRealRoot.re < 132471796 / 100000000 ∧ HexRootsMathlib.Examples.pisotRealRoot.im = 0 ∧ ∀ z ∈ (HexRootsMathlib.toPolyℂ HexRootsMathlib.Examples.pisot).roots.toFinset, z ≠ HexRootsMathlib.Examples.pisotRealRoot → ‖z‖ < 1
A compact statement of the Pisot example: the real root is pinned to eight decimal places and every other root lies strictly inside the unit disc.
The same polynomial drives a runnable demo. From the repository root,
lake exe hexroots_demo
decides that all roots are simple, isolates all three in pairwise-disjoint
dyadic squares, and refines the positive-real isolation to at least 80 bits of
square precision, printing the certified centres and radii. The demo does the
search with the compiled isolator; the theorems above are the kernel-checked
statement of what it found.