Freiman lower construction: priority blockers good
ProvedFreiman.lower_priority_blockers_goodfreimanlower-construction
Every alternative that can block a selected C23 or C20 is itself offered and good, on its actual source branch; the exceptional early-chain alternatives use their inherited A9, word-domain and geometry conditions.
Preamble
import Definitions.Def_Freiman_lowerCertificates import Mathlib.Tactic.Linarith import Mathlib.Tactic.Push open Freiman
Formal statement
theorem Freiman.lower_priority_blockers_good (t : ℝ) (h : ℕ → LowerPair) (n : ℕ) (hh : lowerHistory t h n) : lowerPreferredGood (h n) := by sorry
Source
Freiman's Hall ray: Proof report and corrected English text (8 September 2026), parts/global_selection.tex, two priorities and their admissible geometric alternatives