Report incoming-order repair: middleRepair_cert_interpret_goodness

Proved

Freiman.middleRepair_cert_interpret_goodness

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

freimanhall-rayincoming-ordermiddle

Select the actual child normalization mode and apply the stored goodness-fork comparison in that mode; the independent goodness criterion supplies the automatic opposite cross inequality.

Preamble

import Definitions.Def_Freiman_middleRepairLedger

open Freiman

Formal statement

theorem Freiman.middleRepair_cert_interpret_goodness :
    (∀ 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))) → (∀ (c : MiddleCore) (u v : List ℕ+), middleRegular c → middleDigits123 u → middleDigits123 v →
      0 < u.length+v.length → middleRegular (middleRepairChild c u v) ∧ middleRepairProper c (middleRepairChild c u v)) → (∀ c : MiddleCore, middleRegular c → (middleBounds c).1 ≤ (middleBounds c).2) → ∀ (c : MiddleCore) (f : Fin 9), middleRepairCertDomain c f.val → middleRepairCertActualFamily c f.val → ∀ d ∈ middleRepairRowChildren c (middleCertRow f.val), middleRepairGood d := 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