Perron values have limsup at least two
ProvedFreiman.perron_frequently_at_least_twoclassical-spectracontinued-fractionsfreiman-hall-rayproof-graph
If digits at least two occur infinitely often, P_n exceeds those digits. Otherwise the eventual all-one tail gives P_n→sqrt 5>2, by the report’s cylinder continuity argument.
Preamble
import Definitions.Def_Freiman_perronArithmetic
Formal statement
namespace Freiman
theorem perron_frequently_at_least_two (b : ℕ → ℕ+) :
∀ ε : ℝ, 0 < ε → ∀ N : ℕ, ∃ n : ℕ, N ≤ n ∧ 2 - ε < perronValue b n := by
sorry
end FreimanSource
Freiman's Hall ray: Proof report and corrected English text, 8 September 2026, foundations.tex, §1.2, proof of found:perron