Report incoming-order repair: middleRepair_cert_boundary_pairs_valid
ProvedFreiman.middleRepair_cert_boundary_pairs_validfreimanhall-rayincoming-ordermiddle
Finite applicability of the 146 explicit boundary pointer replacements. Each uses an existing catalog witness and actual L/U premises of the same exact goal/branch/parent conjunction.
Preamble
import Definitions.Def_Freiman_middleRepairLedger open Freiman
Formal statement
theorem Freiman.middleRepair_cert_boundary_pairs_valid :
∀ rec ∈ middleCertData.records, ∀ parent ∈ rec.parents, middleRepairRedirects.find? (fun a => middleRepairRedirectMatches a rec parent) ≠ none → middleRepairRecordValid middleCertData middleRepairRedirects rec parent := by
sorrySource
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.