Freiman lower construction: late short route

Proved

Freiman.lower_late_short_route

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

freimanlower-construction

The exceptional exact parent (31,31) has its separately certified finite good chain; the long-parent r≥13/17 bound is not asserted here.

Preamble

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

open Freiman

Formal statement

theorem Freiman.lower_late_short_route (p : LowerPair) (hp : lowerNormalize p = ([3,1],[3,1])) : ∃ ls : List LowerLabel, lowerLateRouteValid p ls := by
  sorry

Source

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

View graph