Freiman M2B certificate: family mixed A valid
ProvedFreiman.middle_cert_family_mixed_A_validfinite-certificatesfreimanhall-raymiddle
Finite validator for mixed_A: 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_A_valid :
middleCertFamilyValid middleCertData 0 := by
sorrySource
Freiman report (8 September 2026), M2B §§8–9 and complete middle-interval certificate appendix; m2b_readable_model.json, SHA256 a5ac6d3c8e0148e2e3137e8cfa09a2715de6a993dd6ab01eda4842a96bba4cdf.