Freiman repeated-three proof: two width scalar

Proved

Freiman.lowerJ_two_width_scalar

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

certificatesfreimanlower-construction

The explicit endpoint rational enclosures and final rational width margins from the report.

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_two_width_scalar : (1/4:ℝ) < lowerAlpha ∧ lowerAlpha < (27/100:ℝ) ∧ (3/4:ℝ) < lowerBeta ∧ lowerBeta < (4/5:ℝ) ∧ (13243/18000:ℝ)<1 ∧ (739328/796875:ℝ)<1 := 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