Freiman repeated-three proof: contact factor

Proved

Freiman.lowerJ_contact_factor

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

certificatesfreimanlower-construction

The printed S27/S28 are exactly the endpoints of a linear numerator in tau.

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_contact_factor (hn : lowerJSignFacts) (tau : ℝ) (ht : (3/10:ℝ) ≤ tau ∧ tau ≤ (1/3:ℝ)) : (371/500:ℝ) < lowerJCoeff*(1+tau*lowerJC)/(1+tau*lowerJA) := 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