Freiman lower construction: strict good implies good
ProvedFreiman.lower_strict_good_implies_goodfreimanlower-construction
Strict overlap of the two actual closed fork intervals implies nonempty overlap.
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_strict_good_implies_good (p : LowerPair) (h : lowerStrictGood p) : lowerGood 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