theorem helperForTheorem_21_4_originalRoute_univ_convexHullConjugate_zero_neg_of_nonempty_twoBlock {n : ℕ} {I : Type u_1} (f : I → (Fin n → ℝ) → EReal) (I0 : Finset I) (hfProper : ∀ (i : I), ProperConvexFunctionOn Set.univ (f i)) (hfClosed : ∀ (i : I), IsClosed {p : (Fin n → ℝ) × ℝ | f i p.1 ≤ ↑p.2}) (hAffine : ∀ i ∈ I0, ∃ (a : (Fin n → ℝ) →ᵃ[ℝ] ℝ), ∀ (x : Fin n → ℝ), f i x = ↑(a x)) (hConstOutside : ∀ (d : Fin n → ℝ), (∀ (i : I) (x : Fin n → ℝ) (t : ℝ), 0 ≤ t → f i (x + t • d) ≤ f i x) → ∀ i ∉ I0, ∀ (x : Fin n → ℝ) (t : ℝ), 0 ≤ t → f i (x + t • d) = f i x) (hInonempty : ¬IsEmpty I) (hNotPrimal : ¬∃ (x : Fin n → ℝ), ∀ (i : I), f i x ≤ 0) (hA : {x : Fin n → ℝ | ∀ i ∈ I0, f i x ≤ 0}.Nonempty) : ¬IsEmpty { i : I // i ∉ I0 } → (¬∃ x ∈ {x : Fin n → ℝ | ∀ i ∈ I0, f i x ≤ 0}, ∀ (j : { i : I // i ∉ I0 }), f (↑j) x ≤ 0) → convexHullFunctionFamily (fun (i : I) => fenchelConjugate n (f i)) 0 < 0

Helper for Theorem 21.4: the genuine remaining I = I₀ ⊔ I₁ core in the nonempty affine-block branch. At this point C₀ = {x | fᵢ(x) ≤ 0, i ∈ I₀} is nonempty, I₁ is nonempty, and C₀ ∩ C₁ = ∅ with C₁ = {x | fⱼ(x) ≤ 0, j ∈ I₁}.