Freiman.lowerEarlyTerminal_endpoint_equal

Proved

Freiman.lowerEarlyTerminal_endpoint_equal

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

hall-raynumber-theory

Evaluate same-parity endpoint modes and auxiliary shortening with strict right-width normalization, retaining the incoming side at equality.

Preamble

import Definitions.Def_Freiman_lowerEarlyTerminalGeometry

open Freiman

Formal statement

theorem Freiman.lowerEarlyTerminal_endpoint_equal (base : LowerPair) (C : LowerHistoryContext) (hc : C.parity = (false,false))
    (hf : lowerHistoryContextFits base C) (w : LowerPair) (upper : Bool) (he : lowerHistoryWordParity C w false = lowerHistoryWordParity C w true) : ∃ z cs, (z,cs) ∈ section14EndpointCases C w upper ∧ lowerHistoryAtBase base cs ∧
      (0 ≤ certFieldVal z.1 ∧ 0 ≤ certFieldVal z.2) ∧
      lowerHistoryEndpointReal base C w upper = lowerHistoryValue base C z := 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. Source independent_residual.py: equal(); independent_extensions.py: equal().

View graph