Freiman.lowerEarlyTerminal_endpoint_swap_nontie
ProvedFreiman.lowerEarlyTerminal_endpoint_swap_nontiehall-raynumber-theory
Swapping incoming words preserves this endpoint when the ordinary normalization and both possible mixed virtual normalizations avoid full-width equality. No endpoint invariance at a tie is asserted.
Preamble
import Definitions.Def_Freiman_lowerEarlyTerminalGeometry open Freiman
Formal statement
theorem Freiman.lowerEarlyTerminal_endpoint_swap_nontie (w : LowerPair) (hn : LowerEarlyTerminalNoTies w) (upper : Bool) :
lowerEndpoint w upper = lowerEndpoint (w.2,w.1) upper := 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. Endpoint construction lowerEqualWords/lowerEndpointWords, retaining the incoming side at equality.