Freiman.lowerEarlyTerminal_short_applicability

Proved

Freiman.lowerEarlyTerminal_short_applicability

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

hall-raynumber-theory

Translate the unchanged early branch tests to H7/H18/full normalization and the correct H27/H34 cuts, retaining A9 in classes1/2.

Preamble

import Definitions.Def_Freiman_lowerEarlyTerminalGeometry

open Freiman

Formal statement

theorem Freiman.lowerEarlyTerminal_short_applicability (hp : LowerEarlyTerminalParameterLaws) (hdomain : LowerEarlyTerminalDomainLaws)
    (hw : LowerHistoryWidthLaw) (t : ℝ) (p : LowerPair) (hs : lowerState t p) (hd : lowerEarlyDomain p)
    (mode : ℕ) (hm : mode < 2)
    (hbranch : if mode=0 then lowerA p 27 else ¬ lowerA p 27 ∧ lowerA p 34) :
    ∃ i : Fin 3, lowerEarlyTerminalApplied p (lowerEarlyTerminalShortCatalog i) mode := 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