Freiman word guards: case birth313

Proved

Freiman.lower_guard_case_birth313

by tp · Sep 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

freimanword-guards

Transfer the nine finite new-313 checks to actual suffixes. The effective guarded source excludes unguarded 33 and J1 alternatives.

Preamble

import Definitions.Def_Freiman_lowerWordGuardData

open Freiman

Formal statement

theorem Freiman.lower_guard_case_birth313 (p : LowerPair) (c : LowerGuardCase) (hv : lowerGuardCaseValid c) (hf : lowerGuardFits c p)
    (l : LowerLabel) (hl : l ∈ c.labels) (right : Bool)
    (hnew : lowerEnds (lowerSide (lowerChild p l) right) [3,1,3])
    (hchanged : lowerSide (lowerChild p l) right ≠ lowerSide (lowerNormalize p) right) : l = ([2],[3]) := by
  sorry

Source

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.

View graph