Freiman lower construction: equal three source good

Proved

Freiman.lower_equal_three_source_good

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

freimanlower-construction

The actual source criterion (12.8) for equal parity and both ends 3, retaining the source auxiliary e13 endpoint formula. The separately proved source/formal endpoint equivalence transfers the certificate to the formal cover algorithm.

Preamble

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

open Freiman

Formal statement

theorem Freiman.lower_equal_three_source_good (p : LowerPair) (ha : lowerAdmissible p) (hp : ¬ lowerMixed p)
    (hl : lowerEnds p.1 [3]) (hr : lowerEnds p.2 [3]) (hb : lowerParameterBox p)
    (hwide : lowerWidth p.2 ≤ lowerWidth p.1)
    (hratio : lowerWidth p.1 < (19/5 : ℝ)*lowerWidth p.2) : lowerSourceGood p := by
  sorry

Source

Freiman's Hall ray: Proof report and corrected English text (8 September 2026), parts/j_family.tex, lem:equal-three-width; lower_core.tex source endpoint convention

View graph