Freiman word guards: run birth313
ProvedFreiman.lower_guard_run_birth313freimanword-guards
A long repeated-3 continuation ends in 33 on both sides, so cannot create a final 313.
Preamble
import Definitions.Def_Freiman_lowerWordGuardData open Freiman
Formal statement
theorem Freiman.lower_guard_run_birth313 (p : LowerPair) (k : ℕ) (hk : 3 ≤ k) (right : Bool) :
¬ lowerEnds (lowerSide (lowerChild p (List.replicate k 3,List.replicate k 3)) right) [3,1,3] := by
sorrySource
Freiman report, 'The complete boundary table for selected words', Appendix app:selection-words, report/source/staging/parts/word_certificates.tex; global_selection.tex admissibility argument; certificates/word_selection/selection_words_printed.json, word_guards.json and source_bindings.json; verification/families/word_selection/verify_word_guards.py.