Prove2Me

Freiman lower construction: entry chain threeEven

Proved
Freiman.lower_entry_chain_threeEven

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

freimanlower-construction

Glue the six displayed core intervals in the exact source order, using only five adjacent contacts and the H endpoints. Odd classes reverse the order; the terminal2 exception changes the first core endpoint.

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

open Freiman
Formal statement
theorem Freiman.lower_entry_chain_threeEven (p : LowerPair) (hc : lowerEntryContext .threeEven p)
    (hr : lowerEntryRowsHold p (lowerEntryContactRows .threeEven))
    (hcore : ∀ l ∈ lowerEntryLabels, (lowerEntryCore .threeEven p l).Nonempty ∧
      lowerEntryCore .threeEven p l ⊆ lowerCover (lowerChild p l)) :
    lowerEntryH .threeEven p ⊆ {t | ∃ l ∈ lowerEntryLabels, t ∈ lowerCover (lowerChild p l)} := by
  sorry
Source
Freiman's Hall ray: Proof report and corrected English text (8 September 2026), parts/lower_core.tex, prop:lc-H-entry; source H certificate appendix

View graph