Freiman lower construction: other22 birth priority

Proved

Freiman.lower_other22_birth_priority

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

freimanlower-construction

Cancel the actual appended finite words to identify the already selected birth label C23, then use the corresponding earlier stored priority. No future target selection is assumed.

Preamble

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

open Freiman

Formal statement

theorem Freiman.lower_other22_birth_priority (t : ℝ) (h : ℕ → LowerPair) (m : ℕ)
    (hh : lowerHistory t h (m+3))
    (hg : LowerOther22Geometry (h m) (h (m+1)) (h (m+2)) (h (m+3))) :
    lowerPriority t (h m) ([2],[3]) := by
  sorry

Source

Freiman's Hall ray: Proof report and corrected English text (8 September 2026), parts/other22_target.tex, lem:old23-other22-target

View graph