Freiman.lowerEarlyTerminal_child_goodness_from_fork_covers
ProvedFreiman.lowerEarlyTerminal_child_goodness_from_fork_covershall-raynumber-theory
Two strict source cross comparisons and ordered source endpoints give a point in both source forks; the two explicit cover inclusions put that point in both actual forks.
Preamble
import Definitions.Def_Freiman_lowerEarlyTerminalGeometry open Freiman
Formal statement
theorem Freiman.lowerEarlyTerminal_child_goodness_from_fork_covers (p : LowerPair) (l : LowerLabel) (wide : Bool) (norm : CertBound)
(hm : (wide,norm) ∈ section14NormalCases (section14LabelWords l))
(ha : lowerEarlyTerminalAt p [norm])
(ho : ∀ w : LowerPair, lowerEndpoint w false ≤ lowerEndpoint w true)
(hc : ∀ d ∈ ([1,2] : List ℕ+), lowerCover (lowerEarlyTerminalForkPair p l wide d) ⊆
lowerCover (lowerChild (lowerChild p l) ([d],[]))) (h : ∀ req ∈ lowerEarlyTerminalGoodRequirements [] l, lowerEarlyTerminalAt p req.1 →
lowerEarlyTerminalKindHolds p req.2) :
lowerGood (lowerChild p l) := by
sorrySource
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.