Freiman lower construction: other22 priority lower

Proved

Freiman.lower_other22_priority_lower

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

freimanlower-construction

The source C32 lower tails are t31213,t213 while Z lower tails are t3,t213. Their strict first-tail comparison, with actual endpoint rules, gives this local lower anchor.

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_priority_lower (Z B R S : LowerPair) (h : LowerOther22Geometry Z B R S)
    (hn : ¬ lowerEnds Z.1 [3,1]) : lowerLocalLower Z ([3],[2]) < lowerBaseLower Z := 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