Freiman lower construction: entry context auxB

Proved

Freiman.lower_entry_context_auxB

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

freimanlower-construction

Finite terminal suffix and parity classification for family auxB, with the exact H endpoint formula. B at k=0 and auxiliary B are the odd terminal2,3 exception.

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_context_auxB (n k p : ℕ) : ∃ c : LowerEntryClass,
    lowerEntryContext c (lowerNormalize (lowerFamilyPair .auxB n k p)) ∧
    lowerFamilyH .auxB n k p = lowerEntryH c (lowerNormalize (lowerFamilyPair .auxB n k p)) := 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