Freiman lower construction: entry chain twoOdd

Proved

Freiman.lower_entry_chain_twoOdd

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_twoOdd (p : LowerPair) (hc : lowerEntryContext .twoOdd p)
    (hr : lowerEntryRowsHold p (lowerEntryContactRows .twoOdd))
    (hcore : ∀ l ∈ lowerEntryLabels, (lowerEntryCore .twoOdd p l).Nonempty ∧
      lowerEntryCore .twoOdd p l ⊆ lowerCover (lowerChild p l)) :
    lowerEntryH .twoOdd 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