An admissible tail supplies a permitted digit after a matching reference prefix
ProvedFreiman.background_first_difference_candidatecontinued-fractionsmarkov-spectrumnumber-theory
After an initial segment agreeing with the reference word, an admissible tail follows an allowed automaton transition. At an odd zero-based position, digit four is excluded because the previous reference digit is one and 14 is forbidden.
Preamble
import Definitions.Def_Freiman_backgroundWords
Formal statement
namespace Freiman
theorem background_first_difference_candidate (r : Bool) (b : ℕ → ℕ+)
(hb : ∀ n : ℕ, (b n : ℕ) ≤ 4)
(h14 : OneSidedAvoidsBlock b [1,4])
(ha : BackgroundAllowed (backgroundReferenceState r) b)
(n : ℕ) (hp : ∀ k : ℕ, k < n → b k = backgroundReference r k)
(hs : backgroundRun (backgroundReferenceState r)
((List.range n).map (backgroundReference r)) = some (backgroundPhaseState r n)) :
BackgroundCandidate r n (b n) := 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.