Numerical enclosure of Φ

1.685 < Φ < 1.686, from rational enclosures of √2, √11, √22, √(70 + 8√22) and √(17 + 4√22).

theorem LeanPool.CenteredMaximal.phi_mem_Ioo : phi ∈ Set.Ioo (1685 / 1000) (1686 / 1000)

Both numerical bounds on Φ, from rational enclosures of the five square roots.