Freiman.lowerEarlyTerminal_coverage_sound
ProvedFreiman.lowerEarlyTerminal_coverage_soundhall-raynumber-theory
Case analysis over the complete branch catalog converts residual exclusions into every source comparison, with correct strict complements.
Preamble
import Definitions.Def_Freiman_lowerEarlyTerminalGeometry open Freiman
Formal statement
theorem Freiman.lowerEarlyTerminal_coverage_sound (C : LowerEarlyTerminalCatalog) (hc : lowerEarlyTerminalCoverage C) (hr : lowerEarlyTerminalRecordsSound C) : lowerEarlyTerminalGoalsSound C := by sorry
Source
Freiman's Hall ray: Proof report and corrected English text (8 September 2026), pp.120–132, §§ s15:early-residual and s15:terminal-extension; pp.133–139, Proposition l139chain and Appendix app:l139cert.