Freiman repeated-three proof: reverse cross

Proved

Freiman.lowerJ_reverse_cross

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

certificatesfreimanlower-construction

The two componentwise b>φ²(a),φ²(c) source signs give the opposite strict cross comparison.

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_reverse_cross (hn : lowerJSignFacts) (t : ℝ) (p : LowerPair) (hs : lowerState t p) (hr : lowerRunOffered p) (k : ℕ) (hk : 0 < k) : lowerJReverseCross p k := 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