Report incoming-order repair: middleRepair_cert_redirect_keys
ProvedFreiman.middleRepair_cert_redirect_keysfreimanhall-rayincoming-ordermiddle
Every replacement key preserves the original goal, endpoint branch, parent-mode index and source proof ID; the new pointer adds no polynomial.
Preamble
import Definitions.Def_Freiman_middleRepairLedger open Freiman
Formal statement
theorem Freiman.middleRepair_cert_redirect_keys :
∀ a ∈ middleRepairRedirects, ∃ rec ∈ middleCertData.records, a.goal=rec.goal ∧ a.branch=rec.branch ∧ a.parent∈rec.parents ∧ a.originalProof=rec.proof := 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.