Report incoming-order repair: middleRepair_goodness_criterion

Proved

Freiman.middleRepair_goodness_criterion

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

freimanhall-rayincoming-ordermiddle

Report §2: the other cross inequality and endpoint order are componentwise automatic, so goodness is equivalent to its one potentially separating cross inequality. The forks start in the normalized parent order.

Preamble

import Definitions.Def_Freiman_middleRepairLedger

open Freiman

Formal statement

theorem Freiman.middleRepair_goodness_criterion :
    ∀ c : MiddleCore, middleRegular c → (middleRepairGood c ↔ (if (middleNormalized c).left.length%2=0 then (middleBounds (middleRepairChild c [1] [])).1 ≤ (middleBounds (middleRepairChild c [2] [])).2 else (middleBounds (middleRepairChild c [2] [])).1 ≤ (middleBounds (middleRepairChild c [1] [])).2)) := by
  sorry

Source

Freiman report, active m2b_body.tex lines 46–48 and §§2,8–9; immutable M2B coefficient catalog plus the explicit 146-entry incoming-order boundary pointer ledger.

View graph