Freiman.lowerEarlyTerminal_fork_alignment_from_nonties
ProvedFreiman.lowerEarlyTerminal_fork_alignment_from_nontieshall-raynumber-theory
The left-wide branch keeps the incoming order exactly. In the strictly right-wide branch, no ordinary or virtual tie permits endpoint swap symmetry for the two actual grandchildren. The strict source normalization selects the incoming left side at equality.
Preamble
import Definitions.Def_Freiman_lowerEarlyTerminalGeometry open Freiman
Formal statement
theorem Freiman.lowerEarlyTerminal_fork_alignment_from_nonties (p : LowerPair) (l : LowerLabel) (hw : LowerHistoryWidthLaw)
(hswap : ∀ w : LowerPair, LowerEarlyTerminalNoTies w → ∀ upper : Bool,
lowerEndpoint w upper = lowerEndpoint (w.2,w.1) upper)
(hn : ∀ d ∈ ([1,2] : List ℕ+), LowerEarlyTerminalNoTies (lowerEarlyTerminalForkPair p l true d)) :
lowerEarlyTerminalForkAlignment 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.