← Mathematical handbook

The upper seed curves cover every first coordinate

theorem Papers.AnsariRockel2026RhoFootrule.upper_branch_covers_below_one (x : ℝ) (hx : x ∈ Set.Ico 0 1) : ∃ (n : ℕ), ∃ a ∈ Set.Icc 0 (1 / 2), (upperBranch n a).1 = x

theorem Papers.AnsariRockel2026RhoFootrule.upper_seed_at_each_x (x : ℝ) (hx : x ∈ Set.Icc 0 1) : ∃ (y : ℝ), (x, y) ∈ upperSeeds

Every horizontal coordinate in [0,1] occurs in the unconvexified seed set.

theorem Papers.AnsariRockel2026RhoFootrule.directional_region_bounds {p : ℝ × ℝ} (hp : p ∈ directionalRegion) : p.1 ∈ Set.Icc 0 1 ∧ p.2 ∈ Set.Icc 0 1

theorem Papers.AnsariRockel2026RhoFootrule.upper_seeds_projection : Prod.fst '' upperSeeds = Set.Icc 0 1

The projection claim in Proposition 2.10.