Freiman lower construction: run parameter transfer

Proved

Freiman.lower_run_parameter_transfer

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

freimanlower-construction

Exact matrix update sends (r,s,q) to (R_k,S_k,Q_k); the uniform tail-parameter box implies the stated Q bounds and preserves the original width orientation for all k, with ratio below 19/5.

Preamble

import Definitions.Def_Freiman_lowerCertificates
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.Push

open Freiman

Formal statement

theorem Freiman.lower_run_parameter_transfer (htau : ∀ k : ℕ, 0 < k → (3/10 : ℝ) ≤ finiteCF (List.replicate k (3 : ℕ+)) ∧ finiteCF (List.replicate k (3 : ℕ+)) ≤ (1/3 : ℝ))
    (t : ℝ) (p : LowerPair) (hs : lowerState t p) (hr : lowerRunOffered p) : lowerRunParameters p := by
  sorry

Source

Freiman's Hall ray: Proof report and corrected English text (8 September 2026), parts/j_family.tex, eq:j3-updated-parameters and eq:j3-Q-box

View graph