Freiman lower construction: fixed union connected
ProvedFreiman.lower_fixed_union_connectedfreimanlower-construction
The actual closed cover intervals of the 23 roots have a connected union, including the added I2/{2,1} contact.
Preamble
import Definitions.Def_Freiman_lowerCertificates import Mathlib.Tactic.Linarith import Mathlib.Tactic.Push open Freiman
Formal statement
theorem Freiman.lower_fixed_union_connected : IsPreconnected {t : ℝ | ∃ p ∈ lowerFixedRoots, t ∈ lowerCover p} := by
sorrySource
Freiman's Hall ray: Proof report and corrected English text (8 September 2026), parts/lower_core.tex, the 23 strict consecutive contacts