Freiman M2B certificate: witness block 4
ProvedFreiman.middle_cert_witness_block_4finite-certificatesfreimanhall-raymiddle
Exact finite arithmetic validator for source witness IDs 505–630. Retain all coefficients, directions, threshold IDs and printed rational bounds; the two nonzero-direction witnesses use the separate diagonal validator.
Preamble
import Definitions.Def_Freiman_middleCertData import Mathlib.Tactic.FinCases open Freiman
Formal statement
theorem Freiman.middle_cert_witness_block_4 :
∀ w ∈ middleCertWitnesses4, middleCertWitnessValid middleCertData w := by
sorrySource
Freiman report (8 September 2026), M2B §§8–9 and complete middle-interval certificate appendix; m2b_readable_model.json, SHA256 a5ac6d3c8e0148e2e3137e8cfa09a2715de6a993dd6ab01eda4842a96bba4cdf.