Freiman late: late decision sound

Proved

Freiman.late_decision_sound

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

finite-certificatesfreimanhall-raylate

Soundness of complete finite late decision trees, with exact implication premise selection.

Preamble

import Definitions.Def_Freiman_lateGeometry
import Mathlib.Tactic

set_option maxRecDepth 8000
set_option maxHeartbeats 0

open Freiman

Formal statement

theorem Freiman.late_decision_sound : ∀ (C : LateCatalog), lateProofSound C → ∀ right3 bs R tr, lateDecisionValid C right3 bs R tr → lateDecisionSound C right3 bs R := by
  sorry

Source

Freiman report, §15, printed source pages 140–144; active lower_140_144.tex and Appendix Complete finite certificates for printed pages 140–144 (late_certificates.tex); exact late_readable_certificates.json with both original cover_*_certificate.json trees.

View graph