The five suffix states exactly detect the forbidden word 31313
ProvedFreiman.background_automaton_correctcontinued-fractionsmarkov-spectrumnumber-theory
Starting from any of the five proper-prefix states of 31313, the transition process never reaches its forbidden transition exactly when prepending that state's word to the tail produces no occurrence of 31313.
Preamble
import Definitions.Def_Freiman_backgroundWords
Formal statement
namespace Freiman
theorem background_automaton_correct (s : BackgroundState) (b : ℕ → ℕ+) :
BackgroundAllowed s b ↔
OneSidedAvoidsBlock (backgroundPrepend (backgroundStateWord s) b) [3,1,3,1,3] := 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.