theorem helperForTheorem_21_2_affine_nonneg_on_C_and_zero_at_ri_forces_zero_on_C {n : ℕ} (C : Set (Fin n → ℝ)) (x0 : Fin n → ℝ) (hx0ri : x0 ∈ euclideanRelativeInterior_fin n C) (g : (Fin n → ℝ) →ᵃ[ℝ] ℝ) (hg_nonneg : ∀ x ∈ C, 0 ≤ g x) (hg_x0 : g x0 = 0) (x : Fin n → ℝ) : x ∈ C → g x = 0

Helper for Theorem 21.2 (Step 4 route): an affine function that is nonnegative on C and vanishes at a point of ri C must vanish on all of C.

theorem helperForTheorem_21_2_support_nonneg_on_U_of_affineSupport_zero_on_C {n k l : ℕ} (C : Set (Fin n → ℝ)) (fStrict : Fin k → (Fin n → ℝ) → EReal) (fAffine : Fin l → (Fin n → ℝ) → ℝ) (U : Set (Fin l → ℝ)) (hU_def : U = {u : Fin l → ℝ | ∃ x ∈ C, (∀ (i : Fin k), fStrict i x < 0) ∧ ∀ (j : Fin l), fAffine j x ≤ u j}) (lamAffineSupport : Fin l → ℝ) (hlamAffineSupport_nonneg : ∀ (j : Fin l), 0 ≤ lamAffineSupport j) (hAffineSupport_zero_on_C : ∀ x ∈ C, ∑ j : Fin l, lamAffineSupport j * fAffine j x = 0) (u : Fin l → ℝ) : u ∈ U → 0 ≤ ∑ j : Fin l, lamAffineSupport j * u j

Helper for Theorem 21.2: if a nonnegative support combination of the affine block vanishes on all of C, then the same support combination is automatically nonnegative on the strict- feasible affine upper hull U.

theorem helperForTheorem_21_2_boundary_support_oriented_data_on_strictFeasibleAffineUpperHull {l : ℕ} (U : Set (Fin l → ℝ)) (hUconv : Convex ℝ U) (hUupper : ∀ {u v : Fin l → ℝ}, u ∈ U → (∀ (j : Fin l), u j ≤ v j) → v ∈ U) (hUne : U.Nonempty) (_hzeroMemClosureU : (fun (x : Fin l) => 0) ∈ closure U) (hzeroNotMemU : (fun (x : Fin l) => 0) ∉ U) : ∃ (lamAffine : Fin l → ℝ) (β : ℝ), (∀ (j : Fin l), 0 ≤ lamAffine j) ∧ lamAffine ≠ 0 ∧ 0 ≤ β ∧ (∀ u ∈ U, β ≤ u ⬝ᵥ lamAffine) ∧ ∀ (o : Fin l → ℝ), (∀ (j : Fin l), o j < 0) → o ⬝ᵥ lamAffine ≤ β

Helper for Theorem 21.2: from the boundary geometry of the strict-feasible affine upper hull, retain the full oriented separator data against the strict negative orthant rather than only the induced support inequality.

theorem helperForTheorem_21_2_zeroMemU_of_affineSupport_zero_on_C_and_negativeWitnessBridge_in_allShifted_context {n k l : ℕ} (C : Set (Fin n → ℝ)) (fStrict : Fin k → (Fin n → ℝ) → EReal) (fAffine : Fin l → (Fin n → ℝ) → ℝ) (U : Set (Fin l → ℝ)) (hU_def : U = {u : Fin l → ℝ | ∃ x ∈ C, (∀ (i : Fin k), fStrict i x < 0) ∧ ∀ (j : Fin l), fAffine j x ≤ u j}) (lamAffineSupport : Fin l → ℝ) (hlamAffineSupport_nonneg : ∀ (j : Fin l), 0 ≤ lamAffineSupport j) (hzeroNotMemU_to_existsNegativeSupportWitness : (fun (x : Fin l) => 0) ∉ U → ∃ u ∈ U, ∑ j : Fin l, lamAffineSupport j * u j < 0) (hAffineSupport_zero_on_C : ∀ x ∈ C, ∑ j : Fin l, lamAffineSupport j * fAffine j x = 0) : (fun (x : Fin l) => 0) ∈ U

Helper for Theorem 21.2: in the all-shifted branch, if the affine support combination vanishes on C and an external Section 20 / Corollary 7.3.3 bridge supplies a negative-support witness whenever 0 ∉ U, then necessarily 0 ∈ U.

This is the correct dependency-level interface for the remaining geometric step. The earlier attempt to derive 0 ∈ U directly from boundary support data alone was too strong.

def theorem21MixedStrictEqualityImage {n k l : ℕ} (C : Set (Fin n → ℝ)) (fStrict : Fin k → (Fin n → ℝ) → EReal) (fAffine : Fin l → (Fin n → ℝ) → ℝ) : Set (Fin (k + l) → ℝ)

The mixed strict/equality image used in the direct Theorem 20.2 route for Theorem 21.2. The first block records strict upper bounds for the convex constraints, while the second block records the affine constraints exactly.

theorem helperForTheorem_21_2_convexity_of_mixedStrictEqualityImage {n k l : ℕ} (C : Set (Fin n → ℝ)) (hC : Convex ℝ C) (fStrict : Fin k → (Fin n → ℝ) → EReal) (hfStrict : ∀ (i : Fin k), ProperConvexFunctionOn Set.univ (fStrict i)) (fAffine : Fin l → (Fin n → ℝ) → ℝ) (hAffine : ∀ (j : Fin l), ∃ (g : (Fin n → ℝ) →ᵃ[ℝ] ℝ), fAffine j = ⇑g) : Convex ℝ (theorem21MixedStrictEqualityImage C fStrict fAffine)

Helper for Theorem 21.2: the mixed strict/equality image is convex.

theorem helperForTheorem_21_2_nonempty_mixedStrictEqualityImage_of_allShiftedPrimal {n k l : ℕ} (C : Set (Fin n → ℝ)) (fStrict : Fin k → (Fin n → ℝ) → EReal) (fAffine : Fin l → (Fin n → ℝ) → ℝ) (hAllShiftedPrimal : ∀ (ε : ℝ), 0 < ε → ∃ x ∈ C, (∀ (i : Fin k), fStrict i x < 0) ∧ ∀ (j : Fin l), fAffine j x < ε) : (theorem21MixedStrictEqualityImage C fStrict fAffine).Nonempty

Helper for Theorem 21.2: every positive shifted strict-feasible point yields a point in the mixed strict/equality image.

theorem helperForTheorem_21_2_disjoint_mixedStrictEqualityImage_nonpositiveOrthant_of_notPrimal {n k l : ℕ} (C : Set (Fin n → ℝ)) (fStrict : Fin k → (Fin n → ℝ) → EReal) (fAffine : Fin l → (Fin n → ℝ) → ℝ) (hNotPrimal : ¬∃ x ∈ C, (∀ (i : Fin k), fStrict i x < 0) ∧ ∀ (j : Fin l), fAffine j x ≤ 0) : Disjoint (theorem21MixedStrictEqualityImage C fStrict fAffine) {z : Fin (k + l) → ℝ | ∀ (q : Fin (k + l)), z q ≤ 0}

Helper for Theorem 21.2: the mixed strict/equality image is disjoint from the nonpositive orthant exactly when the target primal system is infeasible.

theorem helperForTheorem_21_2_nonpositiveOrthant_nonempty_convex (m : ℕ) : {z : Fin m → ℝ | ∀ (i : Fin m), z i ≤ 0}.Nonempty ∧ Convex ℝ {z : Fin m → ℝ | ∀ (i : Fin m), z i ≤ 0}

Helper for Theorem 21.2: the closed nonpositive orthant in ℝ^m is nonempty and convex.

theorem helperForTheorem_21_2_nonpositiveOrthant_polyhedral (m : ℕ) : IsPolyhedralConvexSet m {z : Fin m → ℝ | ∀ (i : Fin m), z i ≤ 0}

Helper for Theorem 21.2: the closed nonpositive orthant is polyhedral.

theorem helperForTheorem_21_2_targetDual_of_allShiftedPrimal_via_direct_theorem20_2_route {n k l : ℕ} (C : Set (Fin n → ℝ)) (hC : Convex ℝ C) (fStrict : Fin k → (Fin n → ℝ) → EReal) (hfStrict : ∀ (i : Fin k), ProperConvexFunctionOn Set.univ (fStrict i)) (hdomStrict : ∀ (i : Fin k), euclideanRelativeInterior_fin n C ⊆ effectiveDomain Set.univ (fStrict i)) (fAffine : Fin l → (Fin n → ℝ) → ℝ) (hAffine : ∀ (j : Fin l), ∃ (g : (Fin n → ℝ) →ᵃ[ℝ] ℝ), fAffine j = ⇑g) (hFeasRi : ∃ x ∈ euclideanRelativeInterior_fin n C, ∀ (j : Fin l), fAffine j x ≤ 0) (hAllShiftedPrimal : ∀ (ε : ℝ), 0 < ε → ∃ x ∈ C, (∀ (i : Fin k), fStrict i x < 0) ∧ ∀ (j : Fin l), fAffine j x < ε) (hNotPrimal : ¬∃ x ∈ C, (∀ (i : Fin k), fStrict i x < 0) ∧ ∀ (j : Fin l), fAffine j x ≤ 0) : ∃ (lamStrict : Fin k → ℝ) (lamAffine : Fin l → ℝ), (∀ (i : Fin k), 0 ≤ lamStrict i) ∧ (∀ (j : Fin l), 0 ≤ lamAffine j) ∧ (∃ (i : Fin k), lamStrict i ≠ 0) ∧ ∀ x ∈ C, 0 ≤ ∑ i : Fin k, ↑(lamStrict i) * fStrict i x + ∑ j : Fin l, ↑(lamAffine j) * ↑(fAffine j x)

Helper for Theorem 21.2: direct mixed-image route in the all-shifted branch. Instead of passing through the auxiliary upper hull U, apply Theorem 20.2 directly to the mixed strict/equality image and the nonpositive orthant, then promote the resulting separator inequality from ri C to all of C via the Section 21.1 closure machinery.

theorem helperForTheorem_21_2_missing_dependencyLevelBridge_supportNonneg_zeroNotMemU_in_allShifted_context {n k l : ℕ} (C : Set (Fin n → ℝ)) (fStrict : Fin k → (Fin n → ℝ) → EReal) (fAffine : Fin l → (Fin n → ℝ) → ℝ) (U : Set (Fin l → ℝ)) (_hU_def : U = {u : Fin l → ℝ | ∃ x ∈ C, (∀ (i : Fin k), fStrict i x < 0) ∧ ∀ (j : Fin l), fAffine j x ≤ u j}) (_hFeasRi : ∃ x ∈ euclideanRelativeInterior_fin n C, ∀ (j : Fin l), fAffine j x ≤ 0) (_hAllShiftedPrimal : ∀ (ε : ℝ), 0 < ε → ∃ x ∈ C, (∀ (i : Fin k), fStrict i x < 0) ∧ ∀ (j : Fin l), fAffine j x < ε) (_hNotPrimal : ¬∃ x ∈ C, (∀ (i : Fin k), fStrict i x < 0) ∧ ∀ (j : Fin l), fAffine j x ≤ 0) (_hzeroMemClosureU : (fun (x : Fin l) => 0) ∈ closure U) (_hUconv : Convex ℝ U) (_hUupper : ∀ {u v : Fin l → ℝ}, u ∈ U → (∀ (j : Fin l), u j ≤ v j) → v ∈ U) (lamAffineSupport : Fin l → ℝ) (_hlamAffineSupport_nonneg : ∀ (j : Fin l), 0 ≤ lamAffineSupport j) (hExternalDependencyBridge : (∀ u ∈ U, 0 ≤ ∑ j : Fin l, lamAffineSupport j * u j) → (fun (x : Fin l) => 0) ∉ U → False) : (∀ u ∈ U, 0 ≤ ∑ j : Fin l, lamAffineSupport j * u j) → (fun (x : Fin l) => 0) ∉ U → False

Helper for Theorem 21.2: external dependency-level Section 20 / Corollary 7.3.3 bridge in the all-shifted branch, returning the contradiction callback support_nonneg_on_U → (0 ∉ U → False) needed by the local proof.

theorem helperForTheorem_21_2_supportNonneg_on_U_implies_zeroMemU_externalBridge {l : ℕ} (U : Set (Fin l → ℝ)) (_hzeroMemClosureU : (fun (x : Fin l) => 0) ∈ closure U) (_hUconv : Convex ℝ U) (_hUupper : ∀ {u v : Fin l → ℝ}, u ∈ U → (∀ (j : Fin l), u j ≤ v j) → v ∈ U) (lamAffineSupport : Fin l → ℝ) (hSupport_nonneg_on_U : ∀ u ∈ U, 0 ≤ ∑ j : Fin l, lamAffineSupport j * u j) (hSupportNonneg_to_zeroMemU : (∀ u ∈ U, 0 ≤ ∑ j : Fin l, lamAffineSupport j * u j) → (fun (x : Fin l) => 0) ∈ U) : (fun (x : Fin l) => 0) ∈ U

Helper for Theorem 21.2: external closure/support bridge needed in the all-shifted primal branch, upgrading support nonnegativity on U to (fun _ => 0) ∈ U under the boundary-data geometry assumptions.

theorem helperForTheorem_21_2_section20Specialization_supportNonneg_to_zeroMemU_in_allShifted_context {n k l : ℕ} (_C : Set (Fin n → ℝ)) (_fStrict : Fin k → (Fin n → ℝ) → EReal) (_fAffine : Fin l → (Fin n → ℝ) → ℝ) (U : Set (Fin l → ℝ)) (_hU_def : U = {u : Fin l → ℝ | ∃ x ∈ _C, (∀ (i : Fin k), _fStrict i x < 0) ∧ ∀ (j : Fin l), _fAffine j x ≤ u j}) (_hFeasRi : ∃ x ∈ euclideanRelativeInterior_fin n _C, ∀ (j : Fin l), _fAffine j x ≤ 0) (_hAllShiftedPrimal : ∀ (ε : ℝ), 0 < ε → ∃ x ∈ _C, (∀ (i : Fin k), _fStrict i x < 0) ∧ ∀ (j : Fin l), _fAffine j x < ε) (_hNotPrimal : ¬∃ x ∈ _C, (∀ (i : Fin k), _fStrict i x < 0) ∧ ∀ (j : Fin l), _fAffine j x ≤ 0) (_hzeroMemClosureU : (fun (x : Fin l) => 0) ∈ closure U) (_hUconv : Convex ℝ U) (_hUupper : ∀ {u v : Fin l → ℝ}, u ∈ U → (∀ (j : Fin l), u j ≤ v j) → v ∈ U) (lamAffineSupport : Fin l → ℝ) (_hlamAffineSupport_nonneg : ∀ (j : Fin l), 0 ≤ lamAffineSupport j) (hExternalDependencyBridge : (∀ u ∈ U, 0 ≤ ∑ j : Fin l, lamAffineSupport j * u j) → (fun (x : Fin l) => 0) ∉ U → False) : (∀ u ∈ U, 0 ≤ ∑ j : Fin l, lamAffineSupport j * u j) → (fun (x : Fin l) => 0) ∈ U

Helper for Theorem 21.2: missing Section 20 / Corollary 7.3.3 specialization in the all-shifted boundary-data context, upgrading support nonnegativity on U to (fun _ => 0) ∈ U.

theorem helperForTheorem_21_2_externalDependencyBridge_from_section20_specialization_in_allShifted_context {n k l : ℕ} (C : Set (Fin n → ℝ)) (fStrict : Fin k → (Fin n → ℝ) → EReal) (fAffine : Fin l → (Fin n → ℝ) → ℝ) (U : Set (Fin l → ℝ)) (_hU_def : U = {u : Fin l → ℝ | ∃ x ∈ C, (∀ (i : Fin k), fStrict i x < 0) ∧ ∀ (j : Fin l), fAffine j x ≤ u j}) (_hFeasRi : ∃ x ∈ euclideanRelativeInterior_fin n C, ∀ (j : Fin l), fAffine j x ≤ 0) (_hAllShiftedPrimal : ∀ (ε : ℝ), 0 < ε → ∃ x ∈ C, (∀ (i : Fin k), fStrict i x < 0) ∧ ∀ (j : Fin l), fAffine j x < ε) (_hNotPrimal : ¬∃ x ∈ C, (∀ (i : Fin k), fStrict i x < 0) ∧ ∀ (j : Fin l), fAffine j x ≤ 0) (_hzeroMemClosureU : (fun (x : Fin l) => 0) ∈ closure U) (_hUconv : Convex ℝ U) (_hUupper : ∀ {u v : Fin l → ℝ}, u ∈ U → (∀ (j : Fin l), u j ≤ v j) → v ∈ U) (lamAffineSupport : Fin l → ℝ) (_hlamAffineSupport_nonneg : ∀ (j : Fin l), 0 ≤ lamAffineSupport j) (hSection20Specialization : (∀ u ∈ U, 0 ≤ ∑ j : Fin l, lamAffineSupport j * u j) → (fun (x : Fin l) => 0) ∈ U) : (∀ u ∈ U, 0 ≤ ∑ j : Fin l, lamAffineSupport j * u j) → (fun (x : Fin l) => 0) ∉ U → False

Helper for Theorem 21.2: compose the all-shifted Section 20 specialization support_nonneg_on_U → (fun _ => 0) ∈ U into the contradiction callback support_nonneg_on_U → ((fun _ => 0) ∉ U → False) used by local adapters.

theorem helperForTheorem_21_2_zeroMemU_of_boundaryData_support_nonneg_and_externalCallback {n k l : ℕ} (C : Set (Fin n → ℝ)) (fStrict : Fin k → (Fin n → ℝ) → EReal) (fAffine : Fin l → (Fin n → ℝ) → ℝ) (U : Set (Fin l → ℝ)) (hU_def : U = {u : Fin l → ℝ | ∃ x ∈ C, (∀ (i : Fin k), fStrict i x < 0) ∧ ∀ (j : Fin l), fAffine j x ≤ u j}) (hzeroMemClosureU : (fun (x : Fin l) => 0) ∈ closure U) (hUconv : Convex ℝ U) (hUupper : ∀ {u v : Fin l → ℝ}, u ∈ U → (∀ (j : Fin l), u j ≤ v j) → v ∈ U) (lamAffineSupport : Fin l → ℝ) (hlamAffineSupport_nonneg : ∀ (j : Fin l), 0 ≤ lamAffineSupport j) (gSupport : (Fin n → ℝ) →ᵃ[ℝ] ℝ) (hgSupport : ∀ (x : Fin n → ℝ), gSupport x = ∑ j : Fin l, lamAffineSupport j * fAffine j x) (hgSupport_nonneg_on_C : ∀ x ∈ C, 0 ≤ gSupport x) (hSupportNonneg_to_zeroMemU : (∀ u ∈ U, 0 ≤ ∑ j : Fin l, lamAffineSupport j * u j) → (fun (x : Fin l) => 0) ∈ U) : (fun (x : Fin l) => 0) ∈ U

Helper for Theorem 21.2: in the boundary-data setup, transport support nonnegativity from C to U and then apply the external closure/support callback to conclude 0 ∈ U.

theorem helperForTheorem_21_2_zeroMemU_of_gSupport_nonneg_on_C_and_externalDependencyBridge_in_allShifted_context {n k l : ℕ} (C : Set (Fin n → ℝ)) (fStrict : Fin k → (Fin n → ℝ) → EReal) (fAffine : Fin l → (Fin n → ℝ) → ℝ) (U : Set (Fin l → ℝ)) (hU_def : U = {u : Fin l → ℝ | ∃ x ∈ C, (∀ (i : Fin k), fStrict i x < 0) ∧ ∀ (j : Fin l), fAffine j x ≤ u j}) (hFeasRi : ∃ x ∈ euclideanRelativeInterior_fin n C, ∀ (j : Fin l), fAffine j x ≤ 0) (hAllShiftedPrimal : ∀ (ε : ℝ), 0 < ε → ∃ x ∈ C, (∀ (i : Fin k), fStrict i x < 0) ∧ ∀ (j : Fin l), fAffine j x < ε) (hNotPrimal : ¬∃ x ∈ C, (∀ (i : Fin k), fStrict i x < 0) ∧ ∀ (j : Fin l), fAffine j x ≤ 0) (hzeroMemClosureU : (fun (x : Fin l) => 0) ∈ closure U) (hUconv : Convex ℝ U) (hUupper : ∀ {u v : Fin l → ℝ}, u ∈ U → (∀ (j : Fin l), u j ≤ v j) → v ∈ U) (lamAffineSupport : Fin l → ℝ) (hlamAffineSupport_nonneg : ∀ (j : Fin l), 0 ≤ lamAffineSupport j) (gSupport : (Fin n → ℝ) →ᵃ[ℝ] ℝ) (hgSupport : ∀ (x : Fin n → ℝ), gSupport x = ∑ j : Fin l, lamAffineSupport j * fAffine j x) (hExternalDependencyBridge : (∀ u ∈ U, 0 ≤ ∑ j : Fin l, lamAffineSupport j * u j) → (fun (x : Fin l) => 0) ∉ U → False) : (∀ x ∈ C, 0 ≤ gSupport x) → (fun (x : Fin l) => 0) ∈ U

Helper for Theorem 21.2: in the all-shifted boundary-data context, once an external Section 20 / Corollary 7.3.3 contradiction bridge is provided, any global nonnegativity witness for gSupport on C yields (fun _ => 0) ∈ U.

theorem helperForTheorem_21_2_section20Bridge_allShifted_gSupportNonnegOnC_contradiction {n k l : ℕ} (C : Set (Fin n → ℝ)) (fStrict : Fin k → (Fin n → ℝ) → EReal) (fAffine : Fin l → (Fin n → ℝ) → ℝ) (U : Set (Fin l → ℝ)) (hU_def : U = {u : Fin l → ℝ | ∃ x ∈ C, (∀ (i : Fin k), fStrict i x < 0) ∧ ∀ (j : Fin l), fAffine j x ≤ u j}) (hFeasRi : ∃ x ∈ euclideanRelativeInterior_fin n C, ∀ (j : Fin l), fAffine j x ≤ 0) (hAllShiftedPrimal : ∀ (ε : ℝ), 0 < ε → ∃ x ∈ C, (∀ (i : Fin k), fStrict i x < 0) ∧ ∀ (j : Fin l), fAffine j x < ε) (hNotPrimal : ¬∃ x ∈ C, (∀ (i : Fin k), fStrict i x < 0) ∧ ∀ (j : Fin l), fAffine j x ≤ 0) (hzeroMemClosureU : (fun (x : Fin l) => 0) ∈ closure U) (hUconv : Convex ℝ U) (hUupper : ∀ {u v : Fin l → ℝ}, u ∈ U → (∀ (j : Fin l), u j ≤ v j) → v ∈ U) (lamAffineSupport : Fin l → ℝ) (hlamAffineSupport_nonneg : ∀ (j : Fin l), 0 ≤ lamAffineSupport j) (gSupport : (Fin n → ℝ) →ᵃ[ℝ] ℝ) (hgSupport : ∀ (x : Fin n → ℝ), gSupport x = ∑ j : Fin l, lamAffineSupport j * fAffine j x) (hExternalDependencyBridge : (∀ u ∈ U, 0 ≤ ∑ j : Fin l, lamAffineSupport j * u j) → (fun (x : Fin l) => 0) ∉ U → False) (hgSupport_nonneg_on_C : ∀ x ∈ C, 0 ≤ ∑ j : Fin l, lamAffineSupport j * fAffine j x) (hzeroNotMemU : (fun (x : Fin l) => 0) ∉ U) : False

Helper for Theorem 21.2: dependency-level Section 20 / Corollary 7.3.3 bridge in the all-shifted boundary-data context.

This is the exact local contradiction form needed in the muStrict = 0 branch: if the support-weighted affine sum is nonnegative on all of C, then 0 ∉ U is impossible.

theorem helperForTheorem_21_2_all_shifted_primal_to_target_dual_via_closure_and_theorem20_2 {n k l : ℕ} (C : Set (Fin n → ℝ)) (hC : Convex ℝ C) (fStrict : Fin k → (Fin n → ℝ) → EReal) (hfStrict : ∀ (i : Fin k), ProperConvexFunctionOn Set.univ (fStrict i)) (hdomStrict : ∀ (i : Fin k), euclideanRelativeInterior_fin n C ⊆ effectiveDomain Set.univ (fStrict i)) (fAffine : Fin l → (Fin n → ℝ) → ℝ) (hAffine : ∀ (j : Fin l), ∃ (g : (Fin n → ℝ) →ᵃ[ℝ] ℝ), fAffine j = ⇑g) (hFeasRi : ∃ x ∈ euclideanRelativeInterior_fin n C, ∀ (j : Fin l), fAffine j x ≤ 0) (hNotPrimal : ¬∃ x ∈ C, (∀ (i : Fin k), fStrict i x < 0) ∧ ∀ (j : Fin l), fAffine j x ≤ 0) (hAllShiftedPrimal : ∀ (ε : ℝ), 0 < ε → ∃ x ∈ C, (∀ (i : Fin k), fStrict i x < 0) ∧ ∀ (j : Fin l), fAffine j x < ε) : ∃ (lamStrict : Fin k → ℝ) (lamAffine : Fin l → ℝ), (∀ (i : Fin k), 0 ≤ lamStrict i) ∧ (∀ (j : Fin l), 0 ≤ lamAffine j) ∧ (∃ (i : Fin k), lamStrict i ≠ 0) ∧ ∀ x ∈ C, 0 ≤ ∑ i : Fin k, ↑(lamStrict i) * fStrict i x + ∑ j : Fin l, ↑(lamAffine j) * ↑(fAffine j x)

Helper for Theorem 21.2: if all positive shifts admit shifted-primal points but the target primal is false, closure/separation (Corollary 7.3.3 + Theorem 20.2 route) should produce a target dual certificate.

theorem helperForTheorem_21_2_notPrimal_branch_dual_exists {n k l : ℕ} (C : Set (Fin n → ℝ)) (hC : Convex ℝ C) (hklPos : 0 < k + l) (fStrict : Fin k → (Fin n → ℝ) → EReal) (hfStrict : ∀ (i : Fin k), ProperConvexFunctionOn Set.univ (fStrict i)) (hdomStrict : ∀ (i : Fin k), euclideanRelativeInterior_fin n C ⊆ effectiveDomain Set.univ (fStrict i)) (fAffine : Fin l → (Fin n → ℝ) → ℝ) (hAffine : ∀ (j : Fin l), ∃ (g : (Fin n → ℝ) →ᵃ[ℝ] ℝ), fAffine j = ⇑g) (hFeasRi : ∃ x ∈ euclideanRelativeInterior_fin n C, ∀ (j : Fin l), fAffine j x ≤ 0) (hNotPrimal : ¬∃ x ∈ C, (∀ (i : Fin k), fStrict i x < 0) ∧ ∀ (j : Fin l), fAffine j x ≤ 0) : ∃ (lamStrict : Fin k → ℝ) (lamAffine : Fin l → ℝ), (∀ (i : Fin k), 0 ≤ lamStrict i) ∧ (∀ (j : Fin l), 0 ≤ lamAffine j) ∧ (∃ (i : Fin k), lamStrict i ≠ 0) ∧ ∀ x ∈ C, 0 ≤ ∑ i : Fin k, ↑(lamStrict i) * fStrict i x + ∑ j : Fin l, ↑(lamAffine j) * ↑(fAffine j x)

Helper for Theorem 21.2: in the branch ¬targetPrimal and 0 < k+l, either obtain one shifted dual witness and convert it, or use the all-shifted-primal closure route.

theorem theorem21_mixed_convex_affine_alternative {n k l : ℕ} (C : Set (Fin n → ℝ)) (hC : Convex ℝ C) (fStrict : Fin k → (Fin n → ℝ) → EReal) (hfStrict : ∀ (i : Fin k), ProperConvexFunctionOn Set.univ (fStrict i)) (hdomStrict : ∀ (i : Fin k), euclideanRelativeInterior_fin n C ⊆ effectiveDomain Set.univ (fStrict i)) (fAffine : Fin l → (Fin n → ℝ) → ℝ) (hAffine : ∀ (j : Fin l), ∃ (g : (Fin n → ℝ) →ᵃ[ℝ] ℝ), fAffine j = ⇑g) (hFeasRi : ∃ x ∈ euclideanRelativeInterior_fin n C, ∀ (j : Fin l), fAffine j x ≤ 0) : Xor' (∃ x ∈ C, (∀ (i : Fin k), fStrict i x < 0) ∧ ∀ (j : Fin l), fAffine j x ≤ 0) (∃ (lamStrict : Fin k → ℝ) (lamAffine : Fin l → ℝ), (∀ (i : Fin k), 0 ≤ lamStrict i) ∧ (∀ (j : Fin l), 0 ≤ lamAffine j) ∧ (∃ (i : Fin k), lamStrict i ≠ 0) ∧ ∀ x ∈ C, 0 ≤ ∑ i : Fin k, ↑(lamStrict i) * fStrict i x + ∑ j : Fin l, ↑(lamAffine j) * ↑(fAffine j x))

Theorem 21.2: Let C be convex, let f₁, ..., f_k be proper convex functions with dom fᵢ ⊇ ri C, and let f_{k+1}, ..., f_m be affine functions such that f_{k+1}(x) ≤ 0, ..., f_m(x) ≤ 0 has a solution in ri C. Then exactly one alternative holds: (a) there exists x ∈ C with f₁(x), ..., f_k(x) < 0 and f_{k+1}(x), ..., f_m(x) ≤ 0; or (b) there are nonnegative multipliers, with at least one multiplier in the first block nonzero, such that the weighted sum is nonnegative on all of C.

Theorem 21.3 geometry shell

theorem helperForTheorem_21_3_nonpositiveSublevel_closed_convex {n : ℕ} (f : (Fin n → ℝ) → EReal) (hfProper : ProperConvexFunctionOn Set.univ f) (hfClosed : IsClosed {p : (Fin n → ℝ) × ℝ | f p.1 ≤ ↑p.2}) : IsClosed {x : Fin n → ℝ | f x ≤ 0} ∧ Convex ℝ {x : Fin n → ℝ | f x ≤ 0}

Helper for Theorem 21.3: the nonpositive sublevel set of a closed proper convex function on ℝⁿ is closed and convex.

theorem helperForTheorem_21_3_sublevel_closed_convex {n : ℕ} (f : (Fin n → ℝ) → EReal) (hfProper : ProperConvexFunctionOn Set.univ f) (hfClosed : IsClosed {p : (Fin n → ℝ) × ℝ | f p.1 ≤ ↑p.2}) (α : ℝ) : IsClosed {x : Fin n → ℝ | f x ≤ ↑α} ∧ Convex ℝ {x : Fin n → ℝ | f x ≤ ↑α}

Helper for Theorem 21.3: every real sublevel set of a closed proper convex function on ℝⁿ is closed and convex. This is the level-α version used in the shifted-shell route.

theorem helperForTheorem_21_3_inter_nonpositiveSublevel_closed_convex {n : ℕ} {I : Type u_1} (C : Set (Fin n → ℝ)) (hCclosed : IsClosed C) (hCconvex : Convex ℝ C) (f : I → (Fin n → ℝ) → EReal) (hfProper : ∀ (i : I), ProperConvexFunctionOn Set.univ (f i)) (hfClosed : ∀ (i : I), IsClosed {p : (Fin n → ℝ) × ℝ | f i p.1 ≤ ↑p.2}) (i : I) : IsClosed (C ∩ {x : Fin n → ℝ | f i x ≤ 0}) ∧ Convex ℝ (C ∩ {x : Fin n → ℝ | f i x ≤ 0})

Helper for Theorem 21.3: intersecting C with one nonpositive sublevel preserves closedness and convexity.

theorem helperForTheorem_21_3_properConvexEReal_of_properConvexFunctionOn_univ {n : ℕ} (f : (Fin n → ℝ) → EReal) (hfProper : ProperConvexFunctionOn Set.univ f) : ProperConvexERealFunction f

Helper for Theorem 21.3: a proper convex function on univ can be viewed as a proper convex EReal-valued function in the Section 14 recession-function API.

theorem helperForTheorem_21_3_lowerSemicontinuous_of_closedEpigraph {n : ℕ} (f : (Fin n → ℝ) → EReal) (hfClosed : IsClosed {p : (Fin n → ℝ) × ℝ | f p.1 ≤ ↑p.2}) : LowerSemicontinuous f

Helper for Theorem 21.3: closed epigraph implies lower semicontinuity.

theorem helperForTheorem_21_3_exists_nonempty_real_sublevel {n : ℕ} (f : (Fin n → ℝ) → EReal) (hfProper : ProperConvexFunctionOn Set.univ f) : ∃ (α : ℝ), {x : Fin n → ℝ | f x ≤ ↑α}.Nonempty

Helper for Theorem 21.3: a proper convex function on univ has a nonempty real sublevel.

theorem helperForTheorem_21_3_recessionConeEReal_eq_recessionCone_some_nonempty_sublevel {n : ℕ} (f : (Fin n → ℝ) → EReal) (hfProper : ProperConvexFunctionOn Set.univ f) (hfClosed : IsClosed {p : (Fin n → ℝ) × ℝ | f p.1 ≤ ↑p.2}) : ∃ (α : ℝ), {x : Fin n → ℝ | f x ≤ ↑α}.Nonempty ∧ recessionConeEReal f = {x : Fin n → ℝ | f x ≤ ↑α}.recessionCone

Helper for Theorem 21.3: for closed proper convex data, recessionConeEReal coincides with the recession cone of some nonempty real sublevel set.

theorem helperForTheorem_21_3_recessionConeEReal_isClosed_fin {n : ℕ} (f : (Fin n → ℝ) → EReal) (hfProper : ProperConvexFunctionOn Set.univ f) (hfClosed : IsClosed {p : (Fin n → ℝ) × ℝ | f p.1 ≤ ↑p.2}) : IsClosed (recessionConeEReal f)

Helper for Theorem 21.3: recessionConeEReal is closed in finite dimensions for closed proper convex data.

theorem helperForTheorem_21_3_nonpositiveSublevel_ray_antitone {n : ℕ} (f : (Fin n → ℝ) → EReal) (hfProper : ProperConvexFunctionOn Set.univ f) (hfClosed : IsClosed {p : (Fin n → ℝ) × ℝ | f p.1 ≤ ↑p.2}) (hsub_nonempty : {x : Fin n → ℝ | f x ≤ 0}.Nonempty) {d : Fin n → ℝ} (hd : d ∈ {x : Fin n → ℝ | f x ≤ 0}.recessionCone) (x : Fin n → ℝ) (t : ℝ) : 0 ≤ t → f (x + t • d) ≤ f x

Helper for Theorem 21.3: a recession direction of the nonpositive sublevel set of a closed proper convex function makes every ray nonincreasing.

theorem helperForTheorem_21_3_sublevel_ray_antitone {n : ℕ} (f : (Fin n → ℝ) → EReal) (hfProper : ProperConvexFunctionOn Set.univ f) (hfClosed : IsClosed {p : (Fin n → ℝ) × ℝ | f p.1 ≤ ↑p.2}) (α : ℝ) (hsub_nonempty : {x : Fin n → ℝ | f x ≤ ↑α}.Nonempty) {d : Fin n → ℝ} (hd : d ∈ {x : Fin n → ℝ | f x ≤ ↑α}.recessionCone) (x : Fin n → ℝ) (t : ℝ) : 0 ≤ t → f (x + t • d) ≤ f x

Helper for Theorem 21.3: a recession direction of any nonempty real sublevel set of a closed proper convex function makes every ray nonincreasing. This is the shifted-level version needed for ε-shell arguments.

theorem helperForTheorem_21_3_noCommonRecession_contradiction_of_common_nonpositiveSublevel {n : ℕ} {I : Type u_1} (C : Set (Fin n → ℝ)) (f : I → (Fin n → ℝ) → EReal) (hfProper : ∀ (i : I), ProperConvexFunctionOn Set.univ (f i)) (hfClosed : ∀ (i : I), IsClosed {p : (Fin n → ℝ) × ℝ | f i p.1 ≤ ↑p.2}) (hNoCommonRecession : ¬∃ (d : Fin n → ℝ), d ≠ 0 ∧ d ∈ C.recessionCone ∧ ∀ (i : I) (x : Fin n → ℝ) (t : ℝ), 0 ≤ t → f i (x + t • d) ≤ f i x) {d : Fin n → ℝ} (hd_ne : d ≠ 0) (hdC : d ∈ C.recessionCone) (hdSub : ∀ (i : I), d ∈ {x : Fin n → ℝ | f i x ≤ 0}.recessionCone) (hsub_nonempty : ∀ (i : I), {x : Fin n → ℝ | f i x ≤ 0}.Nonempty) : False

Helper for Theorem 21.3: any nonzero direction lying in the recession cone of C and in every nonpositive sublevel set would contradict the original no-common-recession hypothesis.

theorem helperForTheorem_21_3_noCommonRecession_contradiction_of_common_sublevel {n : ℕ} {I : Type u_1} (C : Set (Fin n → ℝ)) (f : I → (Fin n → ℝ) → EReal) (hfProper : ∀ (i : I), ProperConvexFunctionOn Set.univ (f i)) (hfClosed : ∀ (i : I), IsClosed {p : (Fin n → ℝ) × ℝ | f i p.1 ≤ ↑p.2}) (hNoCommonRecession : ¬∃ (d : Fin n → ℝ), d ≠ 0 ∧ d ∈ C.recessionCone ∧ ∀ (i : I) (x : Fin n → ℝ) (t : ℝ), 0 ≤ t → f i (x + t • d) ≤ f i x) (α : ℝ) {d : Fin n → ℝ} (hd_ne : d ≠ 0) (hdC : d ∈ C.recessionCone) (hdSub : ∀ (i : I), d ∈ {x : Fin n → ℝ | f i x ≤ ↑α}.recessionCone) (hsub_nonempty : ∀ (i : I), {x : Fin n → ℝ | f i x ≤ ↑α}.Nonempty) : False

Helper for Theorem 21.3: the no-common-recession contradiction is invariant under replacing the nonpositive sublevel sets {fᵢ ≤ 0} by any common real level sets {fᵢ ≤ α}.

theorem helperForTheorem_21_3_primal_of_isEmpty {n : ℕ} {I : Type u_1} (C : Set (Fin n → ℝ)) (hCnonempty : C.Nonempty) (f : I → (Fin n → ℝ) → EReal) (hI : IsEmpty I) : ∃ x ∈ C, ∀ (i : I), f i x ≤ 0

Helper for Theorem 21.3: if the index type is empty, primal feasibility is immediate from nonemptiness of C.

theorem helperForTheorem_21_3_dual_impossible_of_isEmpty {n : ℕ} {I : Type u_1} (C : Set (Fin n → ℝ)) (hCnonempty : C.Nonempty) (f : I → (Fin n → ℝ) → EReal) (hI : IsEmpty I) : ¬∃ (lam : I →₀ ℝ), (∀ (i : I), 0 ≤ lam i) ∧ ∃ (ε : ℝ), 0 < ε ∧ ∀ x ∈ C, ↑ε ≤ ∑ i ∈ lam.support, ↑(lam i) * f i x

Helper for Theorem 21.3: if the index type is empty, no dual certificate can exist, because every finitely-supported multiplier is zero and thus cannot dominate a positive ε.

theorem helperForTheorem_21_3_primal_excludes_dual {n : ℕ} {I : Type u_1} (C : Set (Fin n → ℝ)) (f : I → (Fin n → ℝ) → EReal) (hPrimal : ∃ x ∈ C, ∀ (i : I), f i x ≤ 0) (hDual : ∃ (lam : I →₀ ℝ), (∀ (i : I), 0 ≤ lam i) ∧ ∃ (ε : ℝ), 0 < ε ∧ ∀ x ∈ C, ↑ε ≤ ∑ i ∈ lam.support, ↑(lam i) * f i x) : False

Helper for Theorem 21.3: a primal witness excludes every dual certificate.

theorem helperForTheorem_21_3_finiteDual_margin_to_finsuppDual_margin {n : ℕ} {I : Type u_1} (C : Set (Fin n → ℝ)) (f : I → (Fin n → ℝ) → EReal) (hfinite : ∃ (m : ℕ) (idx : Fin m → I), Function.Injective idx ∧ ∃ (w : Fin m → ℝ), (∀ (j : Fin m), 0 ≤ w j) ∧ ∃ (ε : ℝ), 0 < ε ∧ ∀ x ∈ C, ↑ε ≤ ∑ j : Fin m, ↑(w j) * f (idx j) x) : ∃ (lam : I →₀ ℝ), (∀ (i : I), 0 ≤ lam i) ∧ ∃ (ε : ℝ), 0 < ε ∧ ∀ x ∈ C, ↑ε ≤ ∑ i ∈ lam.support, ↑(lam i) * f i x

Helper for Theorem 21.3: package a finite-index margin certificate into the exact Finsupp dual-certificate shape used in the theorem statement.

theorem helperForTheorem_21_3_finsuppDual_margin_to_finiteDual_margin {n : ℕ} {I : Type u_1} (C : Set (Fin n → ℝ)) (f : I → (Fin n → ℝ) → EReal) (hDual : ∃ (lam : I →₀ ℝ), (∀ (i : I), 0 ≤ lam i) ∧ ∃ (ε : ℝ), 0 < ε ∧ ∀ x ∈ C, ↑ε ≤ ∑ i ∈ lam.support, ↑(lam i) * f i x) : ∃ (m : ℕ) (idx : Fin m → I), Function.Injective idx ∧ ∃ (w : Fin m → ℝ), (∀ (j : Fin m), 0 ≤ w j) ∧ ∃ (ε : ℝ), 0 < ε ∧ ∀ x ∈ C, ↑ε ≤ ∑ j : Fin m, ↑(w j) * f (idx j) x

Helper for Theorem 21.3: convert a Finsupp dual-margin certificate into a finite indexed certificate with injective indexing.

theorem helperForTheorem_21_3_sparseFiniteDual_margin_to_supportBoundedFinsupp_margin {n : ℕ} {I : Type u_1} (C : Set (Fin n → ℝ)) (f : I → (Fin n → ℝ) → EReal) (hfiniteSparse : ∃ m ≤ n + 1, ∃ (idx : Fin m → I), Function.Injective idx ∧ ∃ (w : Fin m → ℝ), (∀ (j : Fin m), 0 ≤ w j) ∧ ∃ (ε : ℝ), 0 < ε ∧ ∀ x ∈ C, ↑ε ≤ ∑ j : Fin m, ↑(w j) * f (idx j) x) : ∃ (lam : I →₀ ℝ), (∀ (i : I), 0 ≤ lam i) ∧ lam.support.card ≤ n + 1 ∧ ∃ (ε : ℝ), 0 < ε ∧ ∀ x ∈ C, ↑ε ≤ ∑ i ∈ lam.support, ↑(lam i) * f i x

Helper for Theorem 21.3: package a sparse finite-index margin certificate into a support-bounded Finsupp certificate, preserving the cardinal bound ≤ n + 1.

theorem helperForTheorem_21_3_finish_bridge_from_sparseFinsupp_margin {n : ℕ} {I : Type u_1} (C : Set (Fin n → ℝ)) (f : I → (Fin n → ℝ) → EReal) (hDualSparse : ∃ (lam : I →₀ ℝ), (∀ (i : I), 0 ≤ lam i) ∧ lam.support.card ≤ n + 1 ∧ ∃ (ε : ℝ), 0 < ε ∧ ∀ x ∈ C, ↑ε ≤ ∑ i ∈ lam.support, ↑(lam i) * f i x) : ∃ (lam : I →₀ ℝ), (∀ (i : I), 0 ≤ lam i) ∧ lam.support.card ≤ n + 1 ∧ ∃ (ε : ℝ), 0 < ε ∧ ∀ x ∈ C, ↑ε ≤ ∑ i ∈ lam.support, ↑(lam i) * f i x

Helper for Theorem 21.3: once the sparse-support endpoint is available, it matches the exact bridge target shape without additional repackaging.

theorem helperForTheorem_21_3_isClosed_finiteIntersection {n : ℕ} {I : Type u_1} (C : I → Set (Fin n → ℝ)) (t : Finset I) (hClosed : ∀ i ∈ t, IsClosed (C i)) : IsClosed (⋂ i ∈ t, C i)

Helper for Theorem 21.3: finite intersections of closed sets remain closed.

theorem helperForTheorem_21_3_convex_finiteIntersection {n : ℕ} {I : Type u_1} (C : I → Set (Fin n → ℝ)) (t : Finset I) (hConv : ∀ i ∈ t, Convex ℝ (C i)) : Convex ℝ (⋂ i ∈ t, C i)

Helper for Theorem 21.3: finite intersections of convex sets remain convex.

theorem helperForTheorem_21_3_bounded_iff_recessionCone_eq_singleton_zero_fin {n : ℕ} (S : Set (Fin n → ℝ)) (hSne : S.Nonempty) (hSclosed : IsClosed S) (hSconv : Convex ℝ S) : Bornology.IsBounded S ↔ S.recessionCone = {0}

Helper for Theorem 21.3: in Fin n → ℝ, boundedness is equivalent to trivial recession cone for nonempty closed convex sets.

theorem helperForTheorem_21_3_recessionCone_isClosed_fin {n : ℕ} (S : Set (Fin n → ℝ)) (hSclosed : IsClosed S) : IsClosed S.recessionCone

Helper for Theorem 21.3: transport closedness of recession cones from Euclidean-space coordinates to the Fin n → ℝ model.

theorem helperForTheorem_21_3_recessionCone_iInter_eq_iInter_fin {n : ℕ} {ι : Type u_1} (C : ι → Set (Fin n → ℝ)) (hCclosed : ∀ (i : ι), IsClosed (C i)) (hCconv : ∀ (i : ι), Convex ℝ (C i)) (hCne : (⋂ (i : ι), C i).Nonempty) : (⋂ (i : ι), C i).recessionCone = ⋂ (i : ι), (C i).recessionCone

Helper for Theorem 21.3: transport recessionCone_iInter_eq_iInter from Euclidean-space coordinates to the Fin n → ℝ model.

theorem helperForTheorem_21_3_recessionCone_inter_eq_fin {n : ℕ} {A B : Set (Fin n → ℝ)} (hAclosed : IsClosed A) (hBclosed : IsClosed B) (hAconv : Convex ℝ A) (hBconv : Convex ℝ B) (hABne : (A ∩ B).Nonempty) : (A ∩ B).recessionCone = A.recessionCone ∩ B.recessionCone

Helper for Theorem 21.3: recession cone of an intersection of two closed convex sets in Fin n → ℝ is the intersection of recession cones.

theorem helperForTheorem_21_3_recessionFiniteInter_eq_finiteRecessionInter {n : ℕ} {I : Type u_1} (C : I → Set (Fin n → ℝ)) (t : Finset I) (hClosed : ∀ i ∈ t, IsClosed (C i)) (hConv : ∀ i ∈ t, Convex ℝ (C i)) (hNonemptyInter : (⋂ i ∈ t, C i).Nonempty) : (⋂ i ∈ t, C i).recessionCone = ⋂ i ∈ t, (C i).recessionCone

Helper for Theorem 21.3: the recession cone of a finite nonempty intersection is the finite intersection of the recession cones.

theorem helperForTheorem_21_3_finite_recession_subfamily_of_global_singleton {n : ℕ} {I : Type u_1} (C : I → Set (Fin n → ℝ)) (hClosed : ∀ (i : I), IsClosed (C i)) (hNoCommon : ⋂ (i : I), (C i).recessionCone = {0}) : ∃ (t : Finset I), ⋂ i ∈ t, (C i).recessionCone = {0}

Helper for Theorem 21.3: compactness on the unit sphere yields a finite subfamily whose recession-cone intersection is already {0}.

theorem helperForTheorem_21_3_exists_finite_restricted_noCommonRecession_subfamily_of_globalNoCommon {n : ℕ} {I : Type u_1} (C : Set (Fin n → ℝ)) (hCclosed : IsClosed C) (f : I → (Fin n → ℝ) → EReal) (hfProper : ∀ (i : I), ProperConvexFunctionOn Set.univ (f i)) (hfClosed : ∀ (i : I), IsClosed {p : (Fin n → ℝ) × ℝ | f i p.1 ≤ ↑p.2}) (hNoCommonRecession : ¬∃ (d : Fin n → ℝ), d ≠ 0 ∧ d ∈ C.recessionCone ∧ ∀ (i : I) (x : Fin n → ℝ) (t : ℝ), 0 ≤ t → f i (x + t • d) ≤ f i x) : ∃ (u : Finset I), ¬∃ (d : Fin n → ℝ), d ≠ 0 ∧ d ∈ C.recessionCone ∧ ∀ (i : ↑↑u) (x : Fin n → ℝ) (t : ℝ), 0 ≤ t → f (↑i) (x + t • d) ≤ f (↑i) x

Helper for Theorem 21.3: the global no-common-recession hypothesis already has a finite restricted subfamily witness. This separates the compactness-on-directions reduction from the later infeasibility/margin extraction.

theorem helperForTheorem_21_3_exists_finite_infeasible_subfamily_of_notPrimal {n : ℕ} {I : Type u_1} (C : Set (Fin n → ℝ)) (hCclosed : IsClosed C) (hCconvex : Convex ℝ C) (f : I → (Fin n → ℝ) → EReal) (hfProper : ∀ (i : I), ProperConvexFunctionOn Set.univ (f i)) (hfClosed : ∀ (i : I), IsClosed {p : (Fin n → ℝ) × ℝ | f i p.1 ≤ ↑p.2}) (hNoCommonRecession : ¬∃ (d : Fin n → ℝ), d ≠ 0 ∧ d ∈ C.recessionCone ∧ ∀ (i : I) (x : Fin n → ℝ) (t : ℝ), 0 ≤ t → f i (x + t • d) ≤ f i x) (hInonempty : ¬IsEmpty I) (hNotPrimal : ¬∃ x ∈ C, ∀ (i : I), f i x ≤ 0) : ∃ (t : Finset I), ¬(⋂ i ∈ t, C ∩ {x : Fin n → ℝ | f i x ≤ 0}).Nonempty

Helper for Theorem 21.3: if the global primal system is infeasible, some finite subsystem is already infeasible. This isolates the infinite-to-finite reduction from the remaining finite-family analytic core.

theorem helperForTheorem_21_3_support_normal_of_upwardClosed_contains_zero_disjoint_negativeOrthant {m : ℕ} (U : Set (Fin m → ℝ)) (hUconv : Convex ℝ U) (hzeroMemU : (fun (x : Fin m) => 0) ∈ U) (hUO_disjoint : Disjoint U {o : Fin m → ℝ | ∀ (j : Fin m), o j < 0}) : ∃ (lam : Fin m → ℝ), (∀ (j : Fin m), 0 ≤ lam j) ∧ lam ≠ 0 ∧ ∀ u ∈ U, 0 ≤ ∑ j : Fin m, lam j * u j

Helper for Theorem 21.3: if an upward-closed convex set contains the origin and is disjoint from the strict negative orthant, then it admits a nonnegative nontrivial support normal at the origin.

theorem helperForTheorem_21_3_restricted_noCommonRecession_of_finite_nonpositiveMembers_and_trivialRecession {n : ℕ} {I : Type u_1} (C : Set (Fin n → ℝ)) (f : I → (Fin n → ℝ) → EReal) (t : Finset I) (hRecZero : ⋂ i ∈ t, (C ∩ {x : Fin n → ℝ | f i x ≤ 0}).recessionCone = {0}) : ¬∃ (d : Fin n → ℝ), d ≠ 0 ∧ d ∈ C.recessionCone ∧ ∀ (i : ↑↑t) (x : Fin n → ℝ) (s : ℝ), 0 ≤ s → f (↑i) (x + s • d) ≤ f (↑i) x

Helper for Theorem 21.3: if the nonpositive sublevel members of a finite family are all nonempty and have trivial common recession cone, then that finite family already satisfies the restricted no-common-recession condition needed by the shifted-shell argument.

theorem helperForTheorem_21_3_exists_positive_shift_infeasible_of_finite_notPrimal_and_noCommonRecession {n : ℕ} {I : Type u_1} (C : Set (Fin n → ℝ)) (hCclosed : IsClosed C) (hCconvex : Convex ℝ C) (f : I → (Fin n → ℝ) → EReal) (hfProper : ∀ (i : I), ProperConvexFunctionOn Set.univ (f i)) (hfClosed : ∀ (i : I), IsClosed {p : (Fin n → ℝ) × ℝ | f i p.1 ≤ ↑p.2}) (t : Finset I) (htNonempty : t.Nonempty) (hNoCommonRestricted : ¬∃ (d : Fin n → ℝ), d ≠ 0 ∧ d ∈ C.recessionCone ∧ ∀ (i : ↑↑t) (x : Fin n → ℝ) (s : ℝ), 0 ≤ s → f (↑i) (x + s • d) ≤ f (↑i) x) (htNotPrimal : ¬(⋂ i ∈ t, C ∩ {x : Fin n → ℝ | f i x ≤ 0}).Nonempty) : ∃ (ε : ℝ), 0 < ε ∧ ¬(⋂ i ∈ t, C ∩ {x : Fin n → ℝ | f i x ≤ ↑ε}).Nonempty

Helper for Theorem 21.3: under the finite restricted no-common-recession package, failure of the zero-level finite primal system forces a positive common level ε whose shifted finite system is already infeasible.

theorem helperForTheorem_21_3_exists_positive_shift_infeasible_of_finite_nonpositiveMembers_and_trivialRecession {n : ℕ} {I : Type u_1} (C : Set (Fin n → ℝ)) (hCclosed : IsClosed C) (hCconvex : Convex ℝ C) (f : I → (Fin n → ℝ) → EReal) (hfProper : ∀ (i : I), ProperConvexFunctionOn Set.univ (f i)) (hfClosed : ∀ (i : I), IsClosed {p : (Fin n → ℝ) × ℝ | f i p.1 ≤ ↑p.2}) (t : Finset I) (htNonempty : t.Nonempty) (hRecZero : ⋂ i ∈ t, (C ∩ {x : Fin n → ℝ | f i x ≤ 0}).recessionCone = {0}) (htNotPrimal : ¬(⋂ i ∈ t, C ∩ {x : Fin n → ℝ | f i x ≤ 0}).Nonempty) : ∃ (ε : ℝ), 0 < ε ∧ ¬(⋂ i ∈ t, C ∩ {x : Fin n → ℝ | f i x ≤ ↑ε}).Nonempty

Helper for Theorem 21.3: under the finite restricted no-common-recession package, failure of the zero-level finite primal system forces a positive common level ε whose shifted finite system is already infeasible.

theorem helperForTheorem_21_3_convexity_of_finiteValueUpperHull {n m : ℕ} (C : Set (Fin n → ℝ)) (hCconvex : Convex ℝ C) (g : Fin m → (Fin n → ℝ) → EReal) (hgProper : ∀ (j : Fin m), ProperConvexFunctionOn Set.univ (g j)) : Convex ℝ {u : Fin m → ℝ | ∃ x ∈ C, ∀ (j : Fin m), g j x ≤ ↑(u j)}

Helper for Theorem 21.3: the finite real upper hull of a finite family of proper convex functions over a convex set C is convex.

theorem helperForTheorem_21_3_upperClosed_finiteValueUpperHull {n m : ℕ} (C : Set (Fin n → ℝ)) (g : Fin m → (Fin n → ℝ) → EReal) {u v : Fin m → ℝ} (hu : u ∈ {u : Fin m → ℝ | ∃ x ∈ C, ∀ (j : Fin m), g j x ≤ ↑(u j)}) (huv : ∀ (j : Fin m), u j ≤ v j) : v ∈ {u : Fin m → ℝ | ∃ x ∈ C, ∀ (j : Fin m), g j x ≤ ↑(u j)}

Helper for Theorem 21.3: the finite real upper hull is upward-closed under coordinatewise order.

theorem helperForTheorem_21_3_zero_not_mem_finiteValueUpperHull_of_infeasible {n m : ℕ} (C : Set (Fin n → ℝ)) (g : Fin m → (Fin n → ℝ) → EReal) (hNotFeasible : ¬(⋂ (j : Fin m), C ∩ {x : Fin n → ℝ | g j x ≤ 0}).Nonempty) : (fun (x : Fin m) => 0) ∉ {u : Fin m → ℝ | ∃ x ∈ C, ∀ (j : Fin m), g j x ≤ ↑(u j)}

Helper for Theorem 21.3: if the zero-level finite primal system is infeasible, then the origin is not contained in the corresponding finite real upper hull.

theorem helperForTheorem_21_3_constant_vector_mem_finiteValueUpperHull {n m : ℕ} (C : Set (Fin n → ℝ)) (g : Fin m → (Fin n → ℝ) → EReal) (hm : 0 < m) (hAllShiftedFeasible : ∀ (ε : ℝ), 0 < ε → (⋂ (j : Fin m), C ∩ {x : Fin n → ℝ | g j x ≤ ↑ε}).Nonempty) (ε : ℝ) : 0 < ε → (fun (x : Fin m) => ε) ∈ {u : Fin m → ℝ | ∃ x ∈ C, ∀ (j : Fin m), g j x ≤ ↑(u j)}

Helper for Theorem 21.3: every positive common real shift that is feasible for a finite family yields the corresponding constant vector in the finite real upper hull.

theorem helperForTheorem_21_3_zero_mem_closure_finiteValueUpperHull {n m : ℕ} (C : Set (Fin n → ℝ)) (g : Fin m → (Fin n → ℝ) → EReal) (hm : 0 < m) (hAllShiftedFeasible : ∀ (ε : ℝ), 0 < ε → (⋂ (j : Fin m), C ∩ {x : Fin n → ℝ | g j x ≤ ↑ε}).Nonempty) : (fun (x : Fin m) => 0) ∈ closure {u : Fin m → ℝ | ∃ x ∈ C, ∀ (j : Fin m), g j x ≤ ↑(u j)}

Helper for Theorem 21.3: if every positive common shift is feasible for a finite family, then the origin lies in the closure of the associated finite real upper hull.

theorem helperForTheorem_21_3_convexity_of_shiftedFiniteValueUpperHull {n m : ℕ} (C : Set (Fin n → ℝ)) (hCconvex : Convex ℝ C) (g : Fin m → (Fin n → ℝ) → EReal) (hgProper : ∀ (j : Fin m), ProperConvexFunctionOn Set.univ (g j)) (ε : ℝ) : Convex ℝ {u : Fin m → ℝ | ∃ x ∈ C, ∀ (j : Fin m), g j x ≤ ↑(u j + ε)}

Helper for Theorem 21.3: the translated finite real upper hull at level ε is convex.

theorem helperForTheorem_21_3_upperClosed_shiftedFiniteValueUpperHull {n m : ℕ} (C : Set (Fin n → ℝ)) (g : Fin m → (Fin n → ℝ) → EReal) (ε : ℝ) {u v : Fin m → ℝ} (hu : u ∈ {u : Fin m → ℝ | ∃ x ∈ C, ∀ (j : Fin m), g j x ≤ ↑(u j + ε)}) (huv : ∀ (j : Fin m), u j ≤ v j) : v ∈ {u : Fin m → ℝ | ∃ x ∈ C, ∀ (j : Fin m), g j x ≤ ↑(u j + ε)}

Helper for Theorem 21.3: the translated finite real upper hull at level ε is upward-closed under coordinatewise order.

theorem helperForTheorem_21_3_nonempty_shiftedFiniteValueUpperHull {n m : ℕ} (C : Set (Fin n → ℝ)) (g : Fin m → (Fin n → ℝ) → EReal) (ε : ℝ) (hUpperHullNonempty : {u : Fin m → ℝ | ∃ x ∈ C, ∀ (j : Fin m), g j x ≤ ↑(u j)}.Nonempty) : {u : Fin m → ℝ | ∃ x ∈ C, ∀ (j : Fin m), g j x ≤ ↑(u j + ε)}.Nonempty

Helper for Theorem 21.3: a witness to the unshifted finite upper hull yields a witness to the translated upper hull at level ε.

theorem helperForTheorem_21_3_zero_not_mem_shiftedFiniteValueUpperHull_of_shiftGap {n m : ℕ} (C : Set (Fin n → ℝ)) (g : Fin m → (Fin n → ℝ) → EReal) (ε : ℝ) (hShiftGap : ¬(⋂ (j : Fin m), C ∩ {x : Fin n → ℝ | g j x ≤ ↑ε}).Nonempty) : (fun (x : Fin m) => 0) ∉ {u : Fin m → ℝ | ∃ x ∈ C, ∀ (j : Fin m), g j x ≤ ↑(u j + ε)}

Helper for Theorem 21.3: infeasibility of the common shifted system means the origin does not belong to the translated finite upper hull.

theorem helperForTheorem_21_3_positive_support_lower_bound_of_upperClosed_zero_not_mem_closure {m : ℕ} (U : Set (Fin m → ℝ)) (hUconv : Convex ℝ U) (hUne : U.Nonempty) (hUupper : ∀ {u v : Fin m → ℝ}, u ∈ U → (∀ (j : Fin m), u j ≤ v j) → v ∈ U) (hzeroNotMemClosureU : (fun (x : Fin m) => 0) ∉ closure U) : ∃ (lam : Fin m → ℝ) (δ : ℝ), (∀ (j : Fin m), 0 ≤ lam j) ∧ lam ≠ 0 ∧ 0 < δ ∧ ∀ u ∈ U, δ ≤ u ⬝ᵥ lam

Helper for Theorem 21.3: if an upper-closed convex set U is nonempty and its closure does not contain the origin, then a strictly positive nonnegative support functional exists on U.

theorem helperForTheorem_21_3_sparseFiniteDual_margin_of_empty_finiteValueUpperHull {n m : ℕ} (C : Set (Fin n → ℝ)) (hCconvex : Convex ℝ C) (g : Fin m → (Fin n → ℝ) → EReal) (hgProper : ∀ (j : Fin m), ProperConvexFunctionOn Set.univ (g j)) (hm : 0 < m) (hUempty : {u : Fin m → ℝ | ∃ x ∈ C, ∀ (j : Fin m), g j x ≤ ↑(u j)} = ∅) : ∃ p ≤ n + 1, ∃ (idx : Fin p → Fin m), Function.Injective idx ∧ ∃ (w : Fin p → ℝ), (∀ (j : Fin p), 0 ≤ w j) ∧ ∃ (ε : ℝ), 0 < ε ∧ ∀ x ∈ C, ↑ε ≤ ∑ j : Fin p, ↑(w j) * g (idx j) x

Helper for Theorem 21.3: if the finite real upper hull is empty, Helly yields a sparse subfamily whose every point in C forces some coordinate to be ⊤; taking unit weights then gives an immediate positive-margin certificate.

theorem helperForTheorem_21_3_sparseFiniteDual_margin_of_single_empty_shifted_sublevel {n p : ℕ} (C : Set (Fin n → ℝ)) (g : Fin p → (Fin n → ℝ) → EReal) (j0 : Fin p) (ε : ℝ) (hε : 0 < ε) (hEmpty : ¬(C ∩ {x : Fin n → ℝ | g j0 x ≤ ↑ε}).Nonempty) : ∃ m ≤ n + 1, ∃ (idx : Fin m → Fin p), Function.Injective idx ∧ ∃ (w : Fin m → ℝ), (∀ (j : Fin m), 0 ≤ w j) ∧ ∃ (ε' : ℝ), 0 < ε' ∧ ∀ x ∈ C, ↑ε' ≤ ∑ j : Fin m, ↑(w j) * g (idx j) x

Helper for Theorem 21.3: if one shifted sublevel is already empty at level ε, a single-coordinate witness gives an immediate sparse positive-margin certificate.

theorem helperForTheorem_21_3_exists_small_shifted_infeasible_subfamily_fin {n p : ℕ} (C : Set (Fin n → ℝ)) (hCclosed : IsClosed C) (hCconvex : Convex ℝ C) (g : Fin p → (Fin n → ℝ) → EReal) (hgProper : ∀ (j : Fin p), ProperConvexFunctionOn Set.univ (g j)) (hgClosed : ∀ (j : Fin p), IsClosed {q : (Fin n → ℝ) × ℝ | g j q.1 ≤ ↑q.2}) (ε : ℝ) (hShiftGap : ¬(⋂ (j : Fin p), C ∩ {x : Fin n → ℝ | g j x ≤ ↑ε}).Nonempty) : ∃ m ≤ n + 1, ∃ (idx : Fin m → Fin p), Function.Injective idx ∧ ¬(⋂ (j : Fin m), C ∩ {x : Fin n → ℝ | g (idx j) x ≤ ↑ε}).Nonempty

Helper for Theorem 21.3: after excluding the easy empty-sublevel and empty-upper-hull branches, Helly yields a shifted-infeasible finite subfamily of cardinal at most n + 1.

theorem helperForTheorem_21_3_exists_small_zero_infeasible_subfamily_fin {n p : ℕ} (C : Set (Fin n → ℝ)) (hCclosed : IsClosed C) (hCconvex : Convex ℝ C) (g : Fin p → (Fin n → ℝ) → EReal) (hgProper : ∀ (j : Fin p), ProperConvexFunctionOn Set.univ (g j)) (hgClosed : ∀ (j : Fin p), IsClosed {q : (Fin n → ℝ) × ℝ | g j q.1 ≤ ↑q.2}) (hZeroGap : ¬(⋂ (j : Fin p), C ∩ {x : Fin n → ℝ | g j x ≤ 0}).Nonempty) : ∃ m ≤ n + 1, ∃ (idx : Fin m → Fin p), Function.Injective idx ∧ ¬(⋂ (j : Fin m), C ∩ {x : Fin n → ℝ | g (idx j) x ≤ 0}).Nonempty

Helper for Theorem 21.3: Helly also yields a zero-level infeasible finite subfamily of cardinality at most n + 1. This is the correct reduction for the final finite analytic core, because a mere positive-shift gap is not enough by itself to force a positive dual margin.

theorem helperForTheorem_21_3_erealWeightedSum_eq_coeRealWeightedSum_of_supportFinite {n p : ℕ} (g : Fin p → (Fin n → ℝ) → EReal) (hgProper : ∀ (j : Fin p), ProperConvexFunctionOn Set.univ (g j)) (lam : Fin p → ℝ) (x : Fin n → ℝ) (hSupportFinite : ∀ (j : Fin p), lam j ≠ 0 → g j x ≠ ⊤) : ∑ j : Fin p, ↑(lam j) * g j x = ↑(∑ j : Fin p, lam j * (g j x).toReal)

Helper for Theorem 21.3: if every active coordinate of x is finite, the weighted EReal sum agrees with the coercion of the corresponding real sum of toReal values.

theorem helperForTheorem_21_3_shiftedEReal_properConvex {n : ℕ} {g : (Fin n → ℝ) → EReal} (hg : ProperConvexFunctionOn Set.univ g) (ε : ℝ) : ProperConvexFunctionOn Set.univ fun (x : Fin n → ℝ) => g x - ↑ε

Helper for Theorem 21.3: subtracting a finite real constant preserves proper convexity.

theorem helperForTheorem_21_3_positive_margin_of_shiftedLowerBound_and_supportExtension {n p : ℕ} (C : Set (Fin n → ℝ)) (g : Fin p → (Fin n → ℝ) → EReal) (hgProper : ∀ (j : Fin p), ProperConvexFunctionOn Set.univ (g j)) (ε : ℝ) (hε : 0 < ε) (lam : Fin p → ℝ) (hlam_nonneg : ∀ (j : Fin p), 0 ≤ lam j) (hlam_ne_zero : lam ≠ 0) (α : ℝ) (hα_nonneg : 0 ≤ α) (hLower : ∀ (u : Fin p → ℝ), (∃ y ∈ C, ∀ (j : Fin p), g j y ≤ ↑(u j + ε)) → α ≤ u ⬝ᵥ lam) (hSupportExtend : ∀ x ∈ C, (∀ (j : Fin p), lam j ≠ 0 → g j x ≠ ⊤) → ∃ (u : Fin p → ℝ), (∃ y ∈ C, ∀ (j : Fin p), g j y ≤ ↑(u j + ε)) ∧ ∀ (j : Fin p), lam j ≠ 0 → u j + ε = (g j x).toReal) : ∃ (ε' : ℝ), 0 < ε' ∧ ∀ x ∈ C, ↑ε' ≤ ∑ j : Fin p, ↑(lam j) * g j x

Helper for Theorem 21.3: once translated-upper-hull geometry yields a real lower bound, the remaining deterministic analytic step is to extend support-finite points of C to shifted upper-hull points with matching active coordinates.

theorem helperForTheorem_21_3_positive_margin_of_shiftedLowerBound_and_fullSupport {n p : ℕ} (C : Set (Fin n → ℝ)) (g : Fin p → (Fin n → ℝ) → EReal) (hgProper : ∀ (j : Fin p), ProperConvexFunctionOn Set.univ (g j)) (hp : 0 < p) (ε : ℝ) (hε : 0 < ε) (lam : Fin p → ℝ) (hlam_pos : ∀ (j : Fin p), 0 < lam j) (α : ℝ) (hα_nonneg : 0 ≤ α) (hLower : ∀ (u : Fin p → ℝ), (∃ y ∈ C, ∀ (j : Fin p), g j y ≤ ↑(u j + ε)) → α ≤ u ⬝ᵥ lam) : ∃ (ε' : ℝ), 0 < ε' ∧ ∀ x ∈ C, ↑ε' ≤ ∑ j : Fin p, ↑(lam j) * g j x

Helper for Theorem 21.3: if the translated finite upper hull admits a lower bound by a strictly positive weight vector on every coordinate, then no support-extension argument is needed. Points outside the common effective domain are automatically handled because some active coordinate contributes ⊤, while common-domain points can be plugged directly into the translated hull.

theorem helperForTheorem_21_3_positive_coord_of_positive_shiftedLowerBound_of_almostNonpositive_point {n p : ℕ} (C : Set (Fin n → ℝ)) (g : Fin p → (Fin n → ℝ) → EReal) (ε : ℝ) (lam : Fin p → ℝ) (hlam_nonneg : ∀ (i : Fin p), 0 ≤ lam i) (δ : ℝ) (hδ_pos : 0 < δ) (hLower : ∀ (u : Fin p → ℝ), (∃ y ∈ C, ∀ (i : Fin p), g i y ≤ ↑(u i + ε)) → δ ≤ u ⬝ᵥ lam) (j : Fin p) (u : Fin p → ℝ) (hu_mem : ∃ y ∈ C, ∀ (i : Fin p), g i y ≤ ↑(u i + ε)) (hu_nonpos : ∀ (i : Fin p), i ≠ j → u i ≤ 0) : 0 < lam j

Helper for Theorem 21.3: in the strictly positive lower-bound branch, any actual translated-upper-hull point whose coordinates are nonpositive off j forces the j-th coefficient of the support vector to be strictly positive.

theorem helperForTheorem_21_3_beta_eq_zero_of_zero_coord_and_almostNonpositive_point {n p : ℕ} (C : Set (Fin n → ℝ)) (g : Fin p → (Fin n → ℝ) → EReal) (ε : ℝ) (lam : Fin p → ℝ) (hlam_nonneg : ∀ (i : Fin p), 0 ≤ lam i) (β : ℝ) (hβ_nonneg : 0 ≤ β) (hLower : ∀ (u : Fin p → ℝ), (∃ y ∈ C, ∀ (i : Fin p), g i y ≤ ↑(u i + ε)) → β ≤ u ⬝ᵥ lam) (j : Fin p) (hj0 : lam j = 0) (u : Fin p → ℝ) (hu_mem : ∃ y ∈ C, ∀ (i : Fin p), g i y ≤ ↑(u i + ε)) (hu_nonpos : ∀ (i : Fin p), i ≠ j → u i ≤ 0) : β = 0

Helper for Theorem 21.3: in the boundary (β ≥ 0) branch, an actual translated-upper-hull point which is nonpositive off j shows that any zero coefficient at j forces β = 0.

def theorem21ShiftedExtendedUpperHull {n p : ℕ} (C : Set (Fin n → ℝ)) (g : Fin p → (Fin n → ℝ) → EReal) (ε : ℝ) : Set (Fin p → EReal)

The extended translated upper hull used in the last Theorem 21.3 support-upgrade step. Unlike the real upper hull, this version also records witnesses with some coordinates equal to ⊤, which is exactly what the erase-feasible data naturally produces.

theorem helperForTheorem_21_3_singleTop_mem_shiftedExtendedUpperHull_of_eraseFeasible {n p : ℕ} (C : Set (Fin n → ℝ)) (g : Fin p → (Fin n → ℝ) → EReal) (ε : ℝ) (hSublevelNonempty : ∀ (j : Fin p), (C ∩ {x : Fin n → ℝ | g j x ≤ ↑ε}).Nonempty) (hEraseFeasible : ∀ (j : Fin p), (⋂ (i : { i : Fin p // i ≠ j }), C ∩ {x : Fin n → ℝ | g (↑i) x ≤ ↑ε}).Nonempty) (j : Fin p) : have uTop := fun (i : Fin p) => if i = j then ⊤ else 0; uTop ∈ theorem21ShiftedExtendedUpperHull C g ε ∧ uTop j = ⊤ ∧ ∀ (i : Fin p), i ≠ j → uTop i = 0

Helper for Theorem 21.3: erase-feasibility gives a canonical single-top point of the extended translated upper hull. All deleted coordinates are 0, while the retained coordinate is allowed to be ⊤. This is the precise extended-valued witness behind the remaining full-support upgrade gap.

theorem helperForTheorem_21_3_erealWeightedSum_singleTop_eq_zero_of_zero_coord {p : ℕ} (lam : Fin p → ℝ) (j : Fin p) (hj0 : lam j = 0) : (∑ i : Fin p, ↑(lam i) * if i = j then ⊤ else 0) = 0

Helper for Theorem 21.3: the EReal weighted sum of the canonical single-top vector is 0 as soon as the corresponding coefficient vanishes.

theorem helperForTheorem_21_3_nontrivial_shiftedLowerBound_data_of_shiftedUpperHull_geometry {n p : ℕ} (C : Set (Fin n → ℝ)) (hCconvex : Convex ℝ C) (g : Fin p → (Fin n → ℝ) → EReal) (hgProper : ∀ (j : Fin p), ProperConvexFunctionOn Set.univ (g j)) (ε : ℝ) (hShiftGap : ¬(⋂ (j : Fin p), C ∩ {x : Fin n → ℝ | g j x ≤ ↑ε}).Nonempty) (hUpperHullNonempty : {u : Fin p → ℝ | ∃ x ∈ C, ∀ (j : Fin p), g j x ≤ ↑(u j)}.Nonempty) : ∃ (lam : Fin p → ℝ), (∀ (j : Fin p), 0 ≤ lam j) ∧ lam ≠ 0 ∧ ((∃ (β : ℝ), 0 ≤ β ∧ ∀ (u : Fin p → ℝ), (∃ y ∈ C, ∀ (j : Fin p), g j y ≤ ↑(u j + ε)) → β ≤ u ⬝ᵥ lam) ∨ ∃ (δ : ℝ), 0 < δ ∧ ∀ (u : Fin p → ℝ), (∃ y ∈ C, ∀ (j : Fin p), g j y ≤ ↑(u j + ε)) → δ ≤ u ⬝ᵥ lam)

Helper for Theorem 21.3: the genuine remaining finite minimal-core gap is to show that the translated-upper-hull separation data can be upgraded to a separator whose coefficients are strictly positive on every coordinate. Once this is available, the margin extraction is formal and no support-extension bridge is needed.

theorem helperForTheorem_21_3_indicatorEpigraphClosed {n : ℕ} (C : Set (Fin n → ℝ)) (hCclosed : IsClosed C) : IsClosed {p : (Fin n → ℝ) × ℝ | indicatorFunction C p.1 ≤ ↑p.2}

Original-route bridge for Theorem 21.3: this is the genuine remaining second half of Rockafellar's proof. After adjoining the indicator of C, one should define h = conv {fᵢ^*} and its positively homogeneous hull k, prove from ¬primal plus no-common-recession that k(0) = (cl k)(0) = ⊥, hence h(0) < 0, and then feed the Carathéodory/conjugate argument already formalized below.

theorem helperForTheorem_21_3_indicatorMonotoneAlong_d_implies_recessionMembership {n : ℕ} (C : Set (Fin n → ℝ)) {d : Fin n → ℝ} (hmono : ∀ (x : Fin n → ℝ) (t : ℝ), 0 ≤ t → indicatorFunction C (x + t • d) ≤ indicatorFunction C x) : d ∈ C.recessionCone

The indicator monotonicity used in the C-augmentation route is exactly recession-cone membership in C.

theorem helperForTheorem_21_3_originalRoute_univ_convexHullConjugate_zero_neg {n : ℕ} {I : Type u_1} (f : I → (Fin n → ℝ) → EReal) (hfProper : ∀ (i : I), ProperConvexFunctionOn Set.univ (f i)) (hfClosed : ∀ (i : I), IsClosed {p : (Fin n → ℝ) × ℝ | f i p.1 ≤ ↑p.2}) (hNoCommonRecession : ¬∃ (d : Fin n → ℝ), d ≠ 0 ∧ d ∈ Set.univ.recessionCone ∧ ∀ (i : I) (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) : convexHullFunctionFamily (fun (i : I) => fenchelConjugate n (f i)) 0 < 0

Original-route helper for Theorem 21.3: in the C = R^n case, Rockafellar's h := conv {fᵢ^*} satisfies h(0) < 0 under ¬ primal and the no-common-recession hypothesis.

theorem helperForTheorem_21_3_noninjectiveSparseDual_margin_on_univ_to_supportBoundedFinsupp_margin {n : ℕ} {I : Type u_1} (f : I → (Fin n → ℝ) → EReal) (hfinite : ∃ m ≤ n + 1, ∃ (idx : Fin m → I) (w : Fin m → ℝ), (∀ (j : Fin m), 0 ≤ w j) ∧ ∃ (ε : ℝ), 0 < ε ∧ ∀ (x : Fin n → ℝ), ↑ε ≤ ∑ j : Fin m, ↑(w j) * f (idx j) x) : ∃ (lam : I →₀ ℝ), (∀ (i : I), 0 ≤ lam i) ∧ lam.support.card ≤ n + 1 ∧ ∃ (ε : ℝ), 0 < ε ∧ ∀ (x : Fin n → ℝ), ↑ε ≤ ∑ i ∈ lam.support, ↑(lam i) * f i x

Package a sparse nonnegative margin witness on R^n into the support-bounded Finsupp format, allowing a noninjective finite index map and aggregating duplicates fiberwise.

theorem helperForTheorem_21_3_sparse_conjugate_origin_witness_of_convexHullConjugate_zero_neg {n : ℕ} {I : Type u_1} (f : I → (Fin n → ℝ) → EReal) (hfProper : ∀ (i : I), ProperConvexFunctionOn Set.univ (f i)) (hHullZeroNeg : convexHullFunctionFamily (fun (i : I) => fenchelConjugate n (f i)) 0 < 0) : ∃ m ≤ n + 1, ∃ (idx : Fin m → I) (xStar : Fin m → Fin n → ℝ) (w : Fin m → ℝ), IsConvexWeights m w ∧ (∀ (j : Fin m), w j ≠ 0) ∧ 0 = convexCombination n m xStar w ∧ AffineIndependent ℝ xStar ∧ ∑ j : Fin m, ↑(w j) * fenchelConjugate n (f (idx j)) (xStar j) < 0

Local pre-copy of the original-route Carathéodory step, placed before the univ-case bridge so the file can follow Rockafellar's proof order without depending on later declarations.

theorem helperForTheorem_21_3_margin_on_univ_of_sparse_conjugate_origin_witness {n m : ℕ} {I : Type u_1} (f : I → (Fin n → ℝ) → EReal) (hfProper : ∀ (i : I), ProperConvexFunctionOn Set.univ (f i)) (idx : Fin m → I) (xStar : Fin m → Fin n → ℝ) (w : Fin m → ℝ) (hw : IsConvexWeights m w) (hwnz : ∀ (j : Fin m), w j ≠ 0) (hx0 : 0 = convexCombination n m xStar w) (hObjNeg : ∑ j : Fin m, ↑(w j) * fenchelConjugate n (f (idx j)) (xStar j) < 0) : ∃ (ε : ℝ), 0 < ε ∧ ∀ (x : Fin n → ℝ), ↑ε ≤ ∑ j : Fin m, ↑(w j) * f (idx j) x

Local pre-copy of the original-route margin extraction step, placed before the univ-case bridge so the theorem at 4307 can stay on the textbook route.

theorem helperForTheorem_21_3_sparse_dual_margin_on_univ_of_convexHullConjugate_zero_neg {n : ℕ} {I : Type u_1} (f : I → (Fin n → ℝ) → EReal) (hfProper : ∀ (i : I), ProperConvexFunctionOn Set.univ (f i)) (hHullZeroNeg : convexHullFunctionFamily (fun (i : I) => fenchelConjugate n (f i)) 0 < 0) : ∃ m ≤ n + 1, ∃ (idx : Fin m → I) (w : Fin m → ℝ), (∀ (j : Fin m), 0 ≤ w j) ∧ ∃ (ε : ℝ), 0 < ε ∧ ∀ (x : Fin n → ℝ), ↑ε ≤ ∑ j : Fin m, ↑(w j) * f (idx j) x

Local pre-copy of the original-route sparse dual extraction, placed before the univ-case bridge so the bridge itself can use the textbook h(0) < 0 -> Carathéodory -> margin route.

theorem helperForTheorem_21_3_originalRoute_univ_notPrimal_to_supportBoundedFinsupp_margin {n : ℕ} {I : Type u_1} (f : I → (Fin n → ℝ) → EReal) (hfProper : ∀ (i : I), ProperConvexFunctionOn Set.univ (f i)) (hfClosed : ∀ (i : I), IsClosed {p : (Fin n → ℝ) × ℝ | f i p.1 ≤ ↑p.2}) (hNoCommonRecession : ¬∃ (d : Fin n → ℝ), d ≠ 0 ∧ d ∈ Set.univ.recessionCone ∧ ∀ (i : I) (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) : ∃ (lam : I →₀ ℝ), (∀ (i : I), 0 ≤ lam i) ∧ lam.support.card ≤ n + 1 ∧ ∃ (ε : ℝ), 0 < ε ∧ ∀ (x : Fin n → ℝ), ↑ε ≤ ∑ i ∈ lam.support, ↑(lam i) * f i x

Original-route univ-case core for Theorem 21.3. This is the sole remaining second-half bridge after the indicatorFunction C augmentation has been factored out. It should follow the textbook route through

h = conv {fᵢ^*}, the positively homogeneous hull k, Theorems 13.5 and 16.5, the proof that k(0) = (cl k)(0) = ⊥, and finally the sparse Carathéodory/conjugate machinery already proved below.

theorem helperForTheorem_21_3_project_augmentedSupportBoundedFinsupp_margin {n : ℕ} {I : Type u_1} [DecidableEq I] (C : Set (Fin n → ℝ)) (f : I → (Fin n → ℝ) → EReal) (hAug : ∃ (lamAug : Option I →₀ ℝ), (∀ (j : Option I), 0 ≤ lamAug j) ∧ lamAug.support.card ≤ n + 1 ∧ ∃ (ε : ℝ), 0 < ε ∧ ∀ (x : Fin n → ℝ), ↑ε ≤ ∑ j ∈ lamAug.support, ↑(lamAug j) * (match (motive := Option I → (Fin n → ℝ) → EReal) j with | none => indicatorFunction C | some i => f i) x) : ∃ (lam : I →₀ ℝ), (∀ (i : I), 0 ≤ lam i) ∧ lam.support.card ≤ n + 1 ∧ ∃ (ε : ℝ), 0 < ε ∧ ∀ x ∈ C, ↑ε ≤ ∑ i ∈ lam.support, ↑(lam i) * f i x

Project the sparse witness produced on the augmented index type Option I (none = indicatorFunction C) back to the original family indexed by I.

theorem helperForTheorem_21_3_originalRoute_notPrimal_to_supportBoundedFinsupp_margin {n : ℕ} {I : Type u_1} (C : Set (Fin n → ℝ)) (hCnonempty : C.Nonempty) (hCclosed : IsClosed C) (hCconvex : Convex ℝ C) (f : I → (Fin n → ℝ) → EReal) (hfProper : ∀ (i : I), ProperConvexFunctionOn Set.univ (f i)) (hfClosed : ∀ (i : I), IsClosed {p : (Fin n → ℝ) × ℝ | f i p.1 ≤ ↑p.2}) (hNoCommonRecession : ¬∃ (d : Fin n → ℝ), d ≠ 0 ∧ d ∈ C.recessionCone ∧ ∀ (i : I) (x : Fin n → ℝ) (t : ℝ), 0 ≤ t → f i (x + t • d) ≤ f i x) (_hInonempty : ¬IsEmpty I) (hNotPrimal : ¬∃ x ∈ C, ∀ (i : I), f i x ≤ 0) : ∃ (lam : I →₀ ℝ), (∀ (i : I), 0 ≤ lam i) ∧ lam.support.card ≤ n + 1 ∧ ∃ (ε : ℝ), 0 < ε ∧ ∀ x ∈ C, ↑ε ≤ ∑ i ∈ lam.support, ↑(lam i) * f i x

Original-route bridge for Theorem 21.3: this is the genuine remaining second half of Rockafellar's proof. After adjoining the indicator of C, one reduces to the C = R^n core above and then projects the sparse witness back from the augmented index type Option I.

theorem helperForTheorem_21_3_notPrimal_to_finsuppDual_margin_with_supportBound_bridge {n : ℕ} {I : Type u_1} (C : Set (Fin n → ℝ)) (hCnonempty : C.Nonempty) (hCclosed : IsClosed C) (hCconvex : Convex ℝ C) (f : I → (Fin n → ℝ) → EReal) (hfProper : ∀ (i : I), ProperConvexFunctionOn Set.univ (f i)) (hfClosed : ∀ (i : I), IsClosed {p : (Fin n → ℝ) × ℝ | f i p.1 ≤ ↑p.2}) (hNoCommonRecession : ¬∃ (d : Fin n → ℝ), d ≠ 0 ∧ d ∈ C.recessionCone ∧ ∀ (i : I) (x : Fin n → ℝ) (t : ℝ), 0 ≤ t → f i (x + t • d) ≤ f i x) (hInonempty : ¬IsEmpty I) (hNotPrimal : ¬∃ x ∈ C, ∀ (i : I), f i x ≤ 0) : ∃ (lam : I →₀ ℝ), (∀ (i : I), 0 ≤ lam i) ∧ lam.support.card ≤ n + 1 ∧ ∃ (ε : ℝ), 0 < ε ∧ ∀ x ∈ C, ↑ε ≤ ∑ i ∈ lam.support, ↑(lam i) * f i x

Helper for Theorem 21.3: bridge ¬primal plus no-common-recession assumptions to a support-bounded Finsupp dual-margin certificate. This now delegates to the original k / h / conjugate / Carathéodory route.

theorem helperForTheorem_21_3_supportBoundedFinsupp_margin_forget_bound {n : ℕ} {I : Type u_1} (C : Set (Fin n → ℝ)) (f : I → (Fin n → ℝ) → EReal) (hDualSparse : ∃ (lam : I →₀ ℝ), (∀ (i : I), 0 ≤ lam i) ∧ lam.support.card ≤ n + 1 ∧ ∃ (ε : ℝ), 0 < ε ∧ ∀ x ∈ C, ↑ε ≤ ∑ i ∈ lam.support, ↑(lam i) * f i x) : ∃ (lam : I →₀ ℝ), (∀ (i : I), 0 ≤ lam i) ∧ ∃ (ε : ℝ), 0 < ε ∧ ∀ x ∈ C, ↑ε ≤ ∑ i ∈ lam.support, ↑(lam i) * f i x

Helper for Theorem 21.3: forgetting the support-card bound of a sparse Finsupp dual-margin certificate yields the plain dual certificate used in alternative (b).

theorem helperForTheorem_21_3_supportBoundedFinsupp_to_finiteDual_margin {n : ℕ} {I : Type u_1} (C : Set (Fin n → ℝ)) (f : I → (Fin n → ℝ) → EReal) (hDualSparse : ∃ (lam : I →₀ ℝ), (∀ (i : I), 0 ≤ lam i) ∧ lam.support.card ≤ n + 1 ∧ ∃ (ε : ℝ), 0 < ε ∧ ∀ x ∈ C, ↑ε ≤ ∑ i ∈ lam.support, ↑(lam i) * f i x) : ∃ m ≤ n + 1, ∃ (idx : Fin m → I), Function.Injective idx ∧ ∃ (w : Fin m → ℝ), (∀ (j : Fin m), 0 ≤ w j) ∧ ∃ (ε : ℝ), 0 < ε ∧ ∀ x ∈ C, ↑ε ≤ ∑ j : Fin m, ↑(w j) * f (idx j) x

Helper for Theorem 21.3: convert a support-bounded Finsupp margin certificate into a finite-index certificate with injective indexing and the same m ≤ n + 1 bound.

theorem helperForTheorem_21_3_supportBoundedFinsupp_margin_to_finiteAndPlainDual {n : ℕ} {I : Type u_1} (C : Set (Fin n → ℝ)) (f : I → (Fin n → ℝ) → EReal) (hDualSparse : ∃ (lam : I →₀ ℝ), (∀ (i : I), 0 ≤ lam i) ∧ lam.support.card ≤ n + 1 ∧ ∃ (ε : ℝ), 0 < ε ∧ ∀ x ∈ C, ↑ε ≤ ∑ i ∈ lam.support, ↑(lam i) * f i x) : (∃ m ≤ n + 1, ∃ (idx : Fin m → I), Function.Injective idx ∧ ∃ (w : Fin m → ℝ), (∀ (j : Fin m), 0 ≤ w j) ∧ ∃ (ε : ℝ), 0 < ε ∧ ∀ x ∈ C, ↑ε ≤ ∑ j : Fin m, ↑(w j) * f (idx j) x) ∧ ∃ (lam : I →₀ ℝ), (∀ (i : I), 0 ≤ lam i) ∧ ∃ (ε : ℝ), 0 < ε ∧ ∀ x ∈ C, ↑ε ≤ ∑ i ∈ lam.support, ↑(lam i) * f i x

Helper for Theorem 21.3: one sparse Finsupp dual-margin witness can be projected to both downstream dual formats used later in this section (finite/injective and plain Finsupp).

theorem helperForTheorem_21_3_notPrimal_to_finiteDual_margin {n : ℕ} {I : Type u_1} (C : Set (Fin n → ℝ)) (hCnonempty : C.Nonempty) (hCclosed : IsClosed C) (hCconvex : Convex ℝ C) (f : I → (Fin n → ℝ) → EReal) (hfProper : ∀ (i : I), ProperConvexFunctionOn Set.univ (f i)) (hfClosed : ∀ (i : I), IsClosed {p : (Fin n → ℝ) × ℝ | f i p.1 ≤ ↑p.2}) (hNoCommonRecession : ¬∃ (d : Fin n → ℝ), d ≠ 0 ∧ d ∈ C.recessionCone ∧ ∀ (i : I) (x : Fin n → ℝ) (t : ℝ), 0 ≤ t → f i (x + t • d) ≤ f i x) (hInonempty : ¬IsEmpty I) (hNotPrimal : ¬∃ x ∈ C, ∀ (i : I), f i x ≤ 0) : ∃ m ≤ n + 1, ∃ (idx : Fin m → I), Function.Injective idx ∧ ∃ (w : Fin m → ℝ), (∀ (j : Fin m), 0 ≤ w j) ∧ ∃ (ε : ℝ), 0 < ε ∧ ∀ x ∈ C, ↑ε ≤ ∑ j : Fin m, ↑(w j) * f (idx j) x

Helper for Theorem 21.3: extract a finite-index margin certificate from ¬primal.