Freiman lower construction: entry admissible auxB
ProvedFreiman.lower_entry_admissible_auxBfreimanlower-construction
Six actual appended word checks for family auxB: preserve one of the seven oriented central cores and exclude31313. This word claim is separate from numeric goodness.
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_admissible_auxB (n k p : ℕ) : ∀ l ∈ lowerEntryLabels,
lowerAdmissible (lowerChild (lowerFamilyPair .auxB n k p) l) := by
sorrySource
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