A central digit at most three with a neighbor at least two has value below nine halves
ProvedFreiman.background_large_neighborcontinued-fractionsmarkov-spectrumnumber-theory
A fractional tail beginning with a digit at least two is below one half. Together with the other tail below one, this bounds the local value at a digit at most three by nine halves.
Preamble
import Definitions.Def_Freiman_backgroundWords
Formal statement
namespace Freiman
theorem background_large_neighbor (a : ℤ → ℕ+) (i : ℤ) (hi : (a i : ℕ) ≤ 3)
(hn : 2 ≤ (a (i - 1) : ℕ) ∨ 2 ≤ (a (i + 1) : ℕ)) :
localValue a i < (9 / 2 : ℝ) := by
sorry
end FreimanSource
Freiman's Hall ray: Proof report and corrected English text, 8 September 2026, §1.4, Lemma 1.7 and its proof, printed pp. 11–12.