Freiman lower construction: path fairness transfer

Proved

Freiman.lower_path_fairness_transfer

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

freimanlower-construction

Source-list inspection and forced reflections prove that whichever physical side is wider is extended within two steps; the mixed 0,1 case changes parity and cannot repeat.

Preamble

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

open Freiman

Formal statement

theorem Freiman.lower_path_fairness_transfer (hf : ∀ (p : LowerPair), lowerGood p → lowerParameterBox p → let q := lowerNormalize p; lowerWidth (q.1 ++ [2]) < lowerWidth q.2 ∧ lowerWidth (q.1 ++ [3]) < lowerWidth q.2 ∧ lowerWidth (q.1 ++ [1,1]) < lowerWidth q.2 ∧ lowerWidth (q.2 ++ [1]) < lowerWidth q.1)
    (t : ℝ) (h : ℕ → LowerPair) (hh : lowerPath t h) : lowerWithinTwo (lowerPhysicalPath h) := by
  sorry

Source

Freiman's Hall ray: Proof report and corrected English text (8 September 2026), parts/lower_core.tex, lem:lc-both-shrink

View graph