Freiman M2B certificate: pair binding

Proved

Freiman.middle_cert_pair_binding

by tp · Sep 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

finite-certificatesfreimanhall-raymiddle

A validated table witness with direction zero and a valid actual L/U pair supplies exactly the common Bernstein witness format, including its actual strictness flags and all nine i+3j coefficients.

Preamble

import Definitions.Def_Freiman_middleCertData
import Mathlib.Tactic.FinCases

open Freiman

Formal statement

theorem Freiman.middle_cert_pair_binding :
    ∀ (C : MiddleCertCatalog) (p : MiddleCertPair), middleCertWitnessesValid C → middleCertPairValid C p 0 → certWitnessValid (middleCertPairWitness C p) := by
  sorry

Source

Freiman report (8 September 2026), M2B §§8–9 and complete middle-interval certificate appendix; m2b_readable_model.json, SHA256 a5ac6d3c8e0148e2e3137e8cfa09a2715de6a993dd6ab01eda4842a96bba4cdf.

View graph