Freiman lower construction: late entry domain

Proved

Freiman.lower_late_entry_domain

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

freimanlower-construction

An actually reached late parent has r≥13/17 unless its normalized physical pair is exactly (31,31). The early r≤1/3 condition is never imported here.

Preamble

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

open Freiman

Formal statement

theorem Freiman.lower_late_entry_domain (t : ℝ) (h : ℕ → LowerPair) (n : ℕ) (hh : lowerHistory t h n) : lowerLateEntryDomain (h n) := by
  sorry

Source

Freiman's Hall ray: Proof report and corrected English text (8 September 2026), parts/lower_140_144.tex, lem:late-entry-domain