Freiman lower construction: run goodness transfer

Proved

Freiman.lower_run_goodness_transfer

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

freimanlower-construction

Apply the supplied equal-three criterion after the proved parameter update; admissible repeated3 extensions retain the physical central block, both parity cases and width orientation.

Preamble

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

open Freiman

Formal statement

theorem Freiman.lower_run_goodness_transfer (hg : ∀ (p : LowerPair), lowerAdmissible p → ¬ lowerMixed p → lowerEnds p.1 [3] → lowerEnds p.2 [3] → lowerParameterBox p → lowerWidth p.2 ≤ lowerWidth p.1 → lowerWidth p.1 < (19/5 : ℝ)*lowerWidth p.2 → lowerGood p)
    (t : ℝ) (p : LowerPair) (hs : lowerState t p) (hr : lowerRunOffered p) (hb : lowerRunParameters p) :
    ∀ k : ℕ, 0 < k → lowerGood (lowerRunPair p k) := by
  sorry

Source

Freiman's Hall ray: Proof report and corrected English text (8 September 2026), parts/j_family.tex, uniform good run family

View graph