Freiman M2B certificate: family mixed C valid
ProvedFreiman.middle_cert_family_mixed_C_validfinite-certificatesfreimanhall-raymiddle
Finite validator for mixed_C: every native target has its exact stored endpoint/hypothesis match; every grouped record binds its actual pair witnesses and premise conjunction; every nonautomatic branch is covered with all required parent indices.
Preamble
import Definitions.Def_Freiman_middleCertData import Mathlib.Tactic.FinCases open Freiman
Formal statement
theorem Freiman.middle_cert_family_mixed_C_valid :
middleCertFamilyValid middleCertData 2 := by
sorrySource
Freiman report (8 September 2026), M2B §§8–9 and complete middle-interval certificate appendix; m2b_readable_model.json, SHA256 a5ac6d3c8e0148e2e3137e8cfa09a2715de6a993dd6ab01eda4842a96bba4cdf.