Freiman lower construction: selected words

Proved

Freiman.lower_selected_words

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

freimanlower-construction

Every effectively offered child extends the physical words properly with digits 1,2,3 and avoids 31313. This is a word-and-suffix claim, independent of the geometry certificate; numerical auxiliary covers are excluded.

Preamble

import Definitions.Def_Freiman_lowerCertificates
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.Push

open Freiman

Formal statement

theorem Freiman.lower_selected_words (t : ℝ) (h : ℕ → LowerPair) (n : ℕ) (hh : lowerHistory t h n)
    (l : LowerLabel) (hl : lowerOffered (h n) l) :
    lowerAdmissible (lowerChild (h n) l) ∧ lowerExtends (lowerNormalize (h n)) (lowerChild (h n) l) ∧
      lowerPrefixSize (h n) < lowerPrefixSize (lowerChild (h n) l) := by
  sorry

Source

Freiman's Hall ray: Proof report and corrected English text (8 September 2026), parts/global_selection.tex, 422 source/state rows and 2202 candidate checks

View graph