Freiman.lowerEarlyTerminal_cross_contact

Proved

Freiman.lowerEarlyTerminal_cross_contact

by tp · Sep 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

hall-raynumber-theory

Two cross endpoint comparisons plus individual endpoint order give actual interval intersection, with common-parity sign orientation accounted for.

Preamble

import Definitions.Def_Freiman_lowerEarlyTerminalGeometry

open Freiman

Formal statement

theorem Freiman.lowerEarlyTerminal_cross_contact (p : LowerPair) (a b : LowerLabel)
    (ho : ∀ w : LowerPair, lowerEndpoint w false ≤ lowerEndpoint w true)
    (h1 : lowerEarlyTerminalKindHolds p (.compare (section14LabelWords a) true (section14LabelWords b) false false))
    (h2 : lowerEarlyTerminalKindHolds p (.compare (section14LabelWords b) true (section14LabelWords a) false false)) :
    lowerEarlyTerminalContact p a b := 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.

View graph