Freiman.lowerEarlyTerminal_greater_strict

Proved

Freiman.lowerEarlyTerminal_greater_strict

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

hall-raynumber-theory

Strict comparison handles equality, opposite signs and the positive full-width scale explicitly.

Preamble

import Definitions.Def_Freiman_lowerEarlyTerminalGeometry

open Freiman

Formal statement

theorem Freiman.lowerEarlyTerminal_greater_strict (base : LowerPair) (C : LowerHistoryContext) (hc : C.parity = (false,false))
    (hf : lowerHistoryContextFits base C) (x y : CertField × CertField)
    (hx : 0 ≤ certFieldVal x.1 ∧ 0 ≤ certFieldVal x.2)
    (hy : 0 ≤ certFieldVal y.1 ∧ 0 ≤ certFieldVal y.2) : section14ComparisonHolds (lowerEarlyTerminalGreater x y true)
      (lowerRatio base.1) (lowerRatio base.2) (lowerScale base) ↔
        lowerHistoryValue base C y < lowerHistoryValue base C x := 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