Freiman M2B certificate: witness block 3
ProvedFreiman.middle_cert_witness_block_3finite-certificatesfreimanhall-raymiddle
Exact finite arithmetic validator for source witness IDs 379–504. 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_3 :
∀ w ∈ middleCertWitnesses3, 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.