Freiman.lowerEarlyTerminal_terminal_applicability

Proved

Freiman.lowerEarlyTerminal_terminal_applicability

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

hall-raynumber-theory

Translate actual terminal input to its exact catalog conditions. Complemented A27/A34 imply weak source upper bounds; A9 remains explicit for classes1/2.

Preamble

import Definitions.Def_Freiman_lowerEarlyTerminalGeometry

open Freiman

Formal statement

theorem Freiman.lowerEarlyTerminal_terminal_applicability (hp : LowerEarlyTerminalParameterLaws) (hdomain : LowerEarlyTerminalDomainLaws)
    (hw : LowerHistoryWidthLaw) (t : ℝ) (p : LowerPair) (hs : lowerState t p) (hd : lowerEarlyDomain p)
    (h27 : ¬ lowerA p 27) (h34 : ¬ lowerA p 34) (i : Fin 3)
    (he : lowerEnds (lowerNormalize p).1 (lowerEarlyTerminalTerminalCatalog i).leftContext) :
    lowerEarlyTerminalApplied p (lowerEarlyTerminalTerminalCatalog i) 2 := 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