Freiman repeated-three proof: iterate box
ProvedFreiman.lowerJ_iterate_boxcertificatesfreimanlower-construction
The explicit scalar interval map φ([1/4,4/5])⊆[1/4,1/3] and invariant interval induction.
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_iterate_box (r : ℝ) (hr : r ∈ Set.Icc (1/4:ℝ) (4/5)) (k : ℕ) (hk : 0 < k) : (1/4:ℝ) ≤ lowerJIter k r ∧ lowerJIter k r ≤ (1/3:ℝ) := by sorry
Source
Freiman report j_family.tex and j_certificates.tex, equal-three-width and lower-j3-uniform; exact source width-criterion route.