/-
Copyright 2026 The Formal Conjectures Authors.
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
https://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
module
public import Mathlib.Algebra.Polynomial.Roots
public import Mathlib.FieldTheory.Minpoly.Field
public import Mathlib.NumberTheory.Real.GoldenRatio
public import Mathlib.Analysis.Complex.Basic
public import Mathlib.Tactic.ComputeDegree@[expose] public sectionPisot–Vijayaraghavan numbers
A Pisot–Vijayaraghavan number (or PV number) is a real algebraic integer
θ > 1 all of whose Galois conjugates other than θ itself lie strictly
inside the complex unit disc. Equivalently, every root in ℂ of the minimal
polynomial of θ over ℚ, apart from θ, has modulus < 1.
References:
Main definitions
IsPisot: a real number is a Pisot–Vijayaraghavan number.
Main statements
isPisot_goldenRatio: the golden ratio is a Pisot number.
open Polynomial
A Pisot–Vijayaraghavan number is a real algebraic integer θ > 1 all of
whose other conjugates lie strictly inside the complex unit disc: every root in
ℂ of the minimal polynomial of θ over ℚ, except θ itself, has
modulus < 1.
def IsPisot (θ : ℝ) : Prop :=
1 < θ ∧ IsIntegral ℤ θ ∧ ∀ z ∈ (minpoly ℚ θ).aroots ℂ, z ≠ (θ : ℂ) → ‖z‖ < 1open Real in
The golden ratio φ = (1 + √5) / 2 is a Pisot number: it is an algebraic
integer greater than 1, its minimal polynomial over ℚ is X ^ 2 - X - 1, and
its only other conjugate ψ = (1 - √5) / 2 has modulus (√5 - 1) / 2 < 1.
z:ℂhz:map (algebraMap ℚ ℂ) (minpoly ℚ goldenRatio) ≠ 0 ∧ (aeval z) (minpoly ℚ goldenRatio) = 0hzφ:z ≠ ↑goldenRatiog:ℚ[X]hg:X ^ 2 - X - 1 = minpoly ℚ goldenRatio * ghquad:z ^ 2 - z - 1 = 0hsum:↑goldenRatio + ↑goldenConj = 1hprod:↑goldenRatio * ↑goldenConj = -1hfac:(z - ↑goldenRatio) * (z - ↑goldenConj) = 0hzψ:z = ↑goldenConj⊢ -1 < goldenConj ∧ goldenConj < 1
exact ⟨neg_one_lt_goldenConj, z:ℂhz:map (algebraMap ℚ ℂ) (minpoly ℚ goldenRatio) ≠ 0 ∧ (aeval z) (minpoly ℚ goldenRatio) = 0hzφ:z ≠ ↑goldenRatiog:ℚ[X]hg:X ^ 2 - X - 1 = minpoly ℚ goldenRatio * ghquad:z ^ 2 - z - 1 = 0hsum:↑goldenRatio + ↑goldenConj = 1hprod:↑goldenRatio * ↑goldenConj = -1hfac:(z - ↑goldenRatio) * (z - ↑goldenConj) = 0hzψ:z = ↑goldenConj⊢ goldenConj < 1 All goals completed! 🐙⟩