Validity of every equal-IIa certificate record

Proved

Freiman.middle_cert_equal_II_a_records

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

certificatescontinued-fractionshall-ray

Let $\mathcal C$ be the fixed middle-interval certificate catalog, and let $\mathcal R_5$ be its records whose associated goal lies in the equal-IIa family. Then

\forall r\in\mathcal R_5,\quad \operatorname{RecordValid}_{\mathcal C}(r).

Record validity includes valid goal, proof, and branch references, a valid contradiction witness, and membership of each witness bound in the premises for every listed parent. This is the record-validity component of the equal-IIa family certificate theorem.

Preamble

import Definitions.Def_Freiman_middleCertData
open Freiman

Formal statement

theorem Freiman.middle_cert_equal_II_a_records :
    ∀ r ∈ middleCertData.records, (middleCertGoal middleCertData r.goal).family = 5 → middleCertRecordValid middleCertData r := by sorry

Source

Freiman report (8 September 2026), M2B §§8–9 and complete middle-interval certificate appendix; m2b_readable_model.json, SHA256 a5ac6d3c8e0148e2e3137e8cfa09a2715de6a993dd6ab01eda4842a96bba4cdf. Exact component of Def_Freiman_middleCertModel.middleCertFamilyValid at family 5, using the unchanged middleCertData catalog.

View graph