Freiman lower construction: entry cores twoOdd

Proved

Freiman.lower_entry_cores_twoOdd

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

freimanlower-construction

Finite actual endpoint-case adapter for the six explicit cores in class twoOdd. The23 supplied comparisons include all exact periodic-compression equalities and all strict core nonemptiness checks.

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_cores_twoOdd (p : LowerPair) (hc : lowerEntryContext .twoOdd p) (hd : lowerEntryDomain p)
    (ho : lowerEntryChildOrientation p) (hr : lowerEntryRowsHold p (lowerEntryCoreRows .twoOdd)) :
    ∀ l ∈ lowerEntryLabels, (lowerEntryCore .twoOdd p l).Nonempty ∧
      lowerEntryCore .twoOdd p l ⊆ 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