Freiman word guards: source run
ProvedFreiman.lower_guard_source_runfreimanword-guards
Bind the two finite repeated-3 representatives k=1,2 to the actual NN guard. Longer runs are handled by the separate boundary argument.
Preamble
import Definitions.Def_Freiman_lowerWordGuardData open Freiman
Formal statement
theorem Freiman.lower_guard_source_run (p : LowerPair) (hp : lowerAdmissible p) (hr : lowerRunOffered p) (k : ℕ) (hk : 0 < k) (hs : k < 3) :
∃ c ∈ lowerGuardCases, lowerGuardFits c p ∧ (List.replicate k 3,List.replicate k 3) ∈ c.labels := 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.