Freiman lower construction: endpoint completion

Proved

Freiman.lower_endpoint_completion

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

freimanlower-construction

Every actual endpoint, including both virtual parity cases and width ties, is a permitted completion of the old physical prefixes and evaluates to the existing sSup-defined localValue.

Preamble

import Definitions.Def_Freiman_lowerCertificates
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.Push

open Freiman

Formal statement

theorem Freiman.lower_endpoint_completion (p : LowerPair) (h : lowerAdmissible p) (upper : Bool) :
    LowerModel (lowerPeriodicSequence (lowerEndpointWords p upper) [1,2]) ∧
    lowerCylinder p (lowerPeriodicSequence (lowerEndpointWords p upper) [1,2]) ∧
    localValue (lowerPeriodicSequence (lowerEndpointWords p upper) [1,2]) 0 = lowerEndpoint p upper := by
  sorry

Source

Freiman's Hall ray: Proof report and corrected English text (8 September 2026), parts/lower_core.tex, eq:lc-natural-tails and actual endpoint rule

View graph