Freiman repeated-three proof: inner intersection

Proved

Freiman.lowerJ_inner_intersection

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

certificatesfreimanlower-construction

Two ordered real intervals intersect by the two strict cross inequalities; this is a finite order/parity case split.

Preamble

import Definitions.Def_Freiman_lowerJData
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.Push
import Mathlib.Tactic.FinCases

open Freiman

Formal statement

theorem Freiman.lowerJ_inner_intersection (p : LowerPair) (k : ℕ) (ha : lowerJInnerOrder p k) (hb : lowerJInnerOrder p (k+2)) (h1 : lowerJFirstCross p k) (h2 : lowerJReverseCross p k) : (lowerJInner p k ∩ lowerJInner p (k+2)).Nonempty := by
  sorry

Source

Freiman report j_family.tex and j_certificates.tex, equal-three-width and lower-j3-uniform; exact source width-criterion route.

View graph