Freiman repeated-three proof: rectangle
ProvedFreiman.lowerJ_rectanglecertificatesfreimanlower-construction
The report rational rectangle [1/4,4/5]² is nondegenerate.
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_rectangle : certRectangleValid lowerJRectangle := by sorry
Source
Freiman report j_family.tex and j_certificates.tex, equal-three-width and lower-j3-uniform; exact source width-criterion route.