Freiman.lowerEarlyTerminal_terminal3_requirements
ProvedFreiman.lowerEarlyTerminal_terminal3_requirementshall-raynumber-theory
Check that all intervals, child-goodness comparisons, contacts and union alternatives required by each stated route occur among the certified source goals.
Preamble
import Definitions.Def_Freiman_lowerEarlyTerminalGeometry open Freiman
Formal statement
theorem Freiman.lowerEarlyTerminal_terminal3_requirements (mode : ℕ) (hm : mode ∈ [2]) : lowerEarlyTerminalRequirementBinding lowerEarlyTerminalTerminal3 mode := 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. certificates/section15_terminal/geometry_certificate.json (952 records).