Report incoming-order repair: middleRepair_cert_row_hypotheses

Proved

Freiman.middleRepair_cert_row_hypotheses

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

freimanhall-rayincoming-ordermiddle

Translate exactly the existing A/B/S3/S33 row conditions, including their equality assignments, and the uniform 19/5 bound. Only the goodness predicate is the report-normalized one.

Preamble

import Definitions.Def_Freiman_middleRepairLedger

open Freiman

Formal statement

theorem Freiman.middleRepair_cert_row_hypotheses :
    ∀ (c : MiddleCore) (f : Fin 11), middleRepairCertDomain c f.val → decide ((middleNormalized c).left.length%2 ≠ (middleNormalized c).right.length%2) = middleCertParity f.val ∧ middleCertHolds (middleCertFamilyHyp f.val) (middleParameter (middleNormalized c).left) (middleParameter (middleNormalized c).right) (middleQ c) := 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