Freiman.lowerEarlyTerminal_endpoint_order_mixed
ProvedFreiman.lowerEarlyTerminal_endpoint_order_mixedhall-raynumber-theory
The mixed-parity virtual-1 endpoint construction has ordered endpoints.
Preamble
import Definitions.Def_Freiman_lowerEarlyTerminalGeometry open Freiman
Formal statement
theorem Freiman.lowerEarlyTerminal_endpoint_order_mixed (p : LowerPair) (hp : p.1.length % 2 ≠ p.2.length % 2) : lowerEndpoint p false ≤ lowerEndpoint p true := 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. Definitions lowerEndpointWords; full-width normalization and virtual-1 case.