Freiman repeated-three proof: equal endpoints

Proved

Freiman.lowerJ_equal_endpoints

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

certificatesfreimanlower-construction

Explicit four actual source endpoints of J(U1,V) and J(U2,V), with parity duality and the auxiliary-width identity retained.

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_equal_endpoints (haux : ∀ w : List ℕ+, |prefixEval w lowerBeta-prefixEval (w++[1,3]) lowerAlpha| = lowerWidth (w++[1,3])) (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) (hc : lowerJEqualContact p) (hw : lowerWidth ((lowerNormalize p).1++[2]) < lowerWidth (lowerNormalize p).2 ∧ lowerWidth ((lowerNormalize p).1++[1,1]) < lowerWidth (lowerNormalize p).2) : lowerJEqualForkFacts p := 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