Generic objective segments preserve finite endpoint cones and avoid independent simultaneous ties
ProvedHirsch.generic_fibre_objectives_without_independent_tiesLet E be a real vector space, let C0 and C1 be finite lists of strict comparison vectors, and let V be a finite list of nonzero difference vectors. Suppose linear objectives f0 and g0 are strictly negative on C0 and C1 respectively. There exist linear objectives f,g retaining those respective strict comparisons, nonzero on every listed difference, and satisfying
whenever v_i,v_j are linearly independent. Consequently the entire affine objective line has no independent simultaneous ties:
This holds for every real t. For finite Minkowski factors, use the nonzero within-factor point differences as V and the comparisons selecting the desired endpoint vertices in C0,C1. Common strict core comparisons are preserved throughout 0<=t<=1. The result supplies generic-objective existence, not a presumed normal-fan condition. It does not by itself enumerate crossings, assemble their supporting segments, certify Python output, find a decomposition, or prove a uniform graph-diameter bound. Empty comparison lists and empty V are permitted. No finite ambient dimension is assumed.
import Mathlib open Set open scoped BigOperators set_option autoImplicit false
theorem Hirsch.generic_fibre_objectives_without_independent_ties
{E A B I : Type*} [AddCommGroup E] [Module ℝ E]
[Fintype A] [Fintype B] [Fintype I]
(f₀ g₀ : E →ₗ[ℝ] ℝ) (c₀ : A → E) (c₁ : B → E) (v : I → E)
(hc₀ : ∀ a, f₀ (c₀ a) < 0)
(hc₁ : ∀ b, g₀ (c₁ b) < 0)
(hv : ∀ i, v i ≠ 0) :
∃ f g : E →ₗ[ℝ] ℝ,
(∀ a, f (c₀ a) < 0) ∧
(∀ b, g (c₁ b) < 0) ∧
(∀ i, f (v i) ≠ 0) ∧
(∀ i, g (v i) ≠ 0) ∧
(∀ i j, v j ∉ Submodule.span ℝ ({v i} : Set E) →
f (v i)*g (v j)-f (v j)*g (v i) ≠ 0) ∧
∀ (t : ℝ) (i j : I),
((1-t)*f (v i)+t*g (v i)=0) →
((1-t)*f (v j)+t*g (v j)=0) →
v j ∈ Submodule.span ℝ ({v i} : Set E) := by sorry