theorem helperForTheorem_6_30_24_currentPositiveSignTargetStatementFunctionType_not_nonempty : ¬Nonempty (∀ {m n n0 : ℕ} {ni : Fin m → ℕ} (data : IntermediateProgramData m n n0 ni), IsClosedProperConvexERealFunction data.h0 → (∀ (i : Fin m), IsClosedProperConvexERealFunction (data.h i)) → (∀ (xStar : Fin n → ℝ) (wStar : IntermediateProgramDualParameter m n n0 ni), (intermediateProgramDualFeasible data xStar wStar → adjointOfIntermediateProgram data xStar wStar = intermediateProgramDualObjective data wStar) ∧ (¬intermediateProgramDualFeasible data xStar wStar → adjointOfIntermediateProgram data xStar wStar = ⊥)) ∧ dualProgramValueOfIntermediateProgram data = sSup {v : EReal | ∃ (wStar : IntermediateProgramDualParameter m n n0 ni), intermediateProgramDualFeasible data 0 wStar ∧ v = intermediateProgramDualObjective data wStar})

Helper for Theorem 6.30.24: even after changing the feasible-branch sign, the full dependent theorem type is still not inhabited. The zero-multiplier restricted-domain witness specializes any global positive-sign proof term to the impossible equality 0 = -∞.

theorem helperForTheorem_6_30_24_currentPositiveSignTargetStatementFunctionType_isEmpty : IsEmpty (∀ {m n n0 : ℕ} {ni : Fin m → ℕ} (data : IntermediateProgramData m n n0 ni), IsClosedProperConvexERealFunction data.h0 → (∀ (i : Fin m), IsClosedProperConvexERealFunction (data.h i)) → (∀ (xStar : Fin n → ℝ) (wStar : IntermediateProgramDualParameter m n n0 ni), (intermediateProgramDualFeasible data xStar wStar → adjointOfIntermediateProgram data xStar wStar = intermediateProgramDualObjective data wStar) ∧ (¬intermediateProgramDualFeasible data xStar wStar → adjointOfIntermediateProgram data xStar wStar = ⊥)) ∧ dualProgramValueOfIntermediateProgram data = sSup {v : EReal | ∃ (wStar : IntermediateProgramDualParameter m n n0 ni), intermediateProgramDualFeasible data 0 wStar ∧ v = intermediateProgramDualObjective data wStar})

Helper for Theorem 6.30.24: even the sign-only repaired dependent theorem type is empty as a type. This records the zero-multiplier restricted-domain obstruction in the same IsEmpty format already used for the literal negative-sign theorem header.

theorem helperForTheorem_6_30_24_signRepairStillNeedsObjectiveRepair : helperForTheorem_6_30_24_wrongSignWitness_correctedSpecializedConclusionProp ∧ ¬Nonempty (∀ {m n n0 : ℕ} {ni : Fin m → ℕ} (data : IntermediateProgramData m n n0 ni), IsClosedProperConvexERealFunction data.h0 → (∀ (i : Fin m), IsClosedProperConvexERealFunction (data.h i)) → (∀ (xStar : Fin n → ℝ) (wStar : IntermediateProgramDualParameter m n n0 ni), (intermediateProgramDualFeasible data xStar wStar → adjointOfIntermediateProgram data xStar wStar = intermediateProgramDualObjective data wStar) ∧ (¬intermediateProgramDualFeasible data xStar wStar → adjointOfIntermediateProgram data xStar wStar = ⊥)) ∧ dualProgramValueOfIntermediateProgram data = sSup {v : EReal | ∃ (wStar : IntermediateProgramDualParameter m n n0 ni), intermediateProgramDualFeasible data 0 wStar ∧ v = intermediateProgramDualObjective data wStar})

Helper for Theorem 6.30.24: changing only the feasible-branch sign is not enough. The named wrong-sign witness validates the repaired specialization, but the zero-multiplier restricted- domain witness still rules out any global positive-sign theorem term.

theorem helperForTheorem_6_30_24_exists_finiteWitnessFamily {m n n0 : ℕ} {ni : Fin m → ℕ} (data : IntermediateProgramData m n n0 ni) (hh0 : IsClosedProperConvexERealFunction data.h0) (hh : ∀ (i : Fin m), IsClosedProperConvexERealFunction (data.h i)) : ∃ (y0 : Fin n0 → ℝ), data.h0 y0 ≠ ⊤ ∧ ∃ (y : (i : Fin m) → Fin (ni i) → ℝ), ∀ (i : Fin m), data.h i (y i) ≠ ⊤

Helper for Theorem 6.30.24: closed proper convexity supplies one finite witness point for h₀ and one finite witness point for each hᵢ.

theorem helperForTheorem_6_30_24_dualObjective_ne_top_of_nonnegative {m n n0 : ℕ} {ni : Fin m → ℕ} (data : IntermediateProgramData m n n0 ni) (hh0 : IsClosedProperConvexERealFunction data.h0) (hh : ∀ (i : Fin m), IsClosedProperConvexERealFunction (data.h i)) (wStar : IntermediateProgramDualParameter m n n0 ni) (hnonneg : ∀ (i : Fin m), 0 ≤ wStar.vStar i) : intermediateProgramDualObjective data wStar ≠ ⊤

Helper for Theorem 6.30.24: on the nonnegative branch, every Fenchel-conjugate term in the explicit dual objective stays away from -∞, so the whole objective stays away from +∞.

theorem helperForTheorem_6_30_24_negativeMultiplierRayWitnessValue {m n n0 : ℕ} {ni : Fin m → ℕ} (data : IntermediateProgramData m n n0 ni) (xStar : Fin n → ℝ) (wStar : IntermediateProgramDualParameter m n n0 ni) (w0 : IntermediateProgramParameter m n n0 ni) (x0 : Fin n → ℝ) (hxFeas : x0 ∈ intermediateProgramFeasibleSet data w0) (i0 : Fin m) (t : ℝ) (ht : 0 ≤ t) : have w := { v := w0.v + Pi.single i0 t, p0 := w0.p0, p := w0.p }; intermediateProgramBifunction data w x0 - ↑(x0 ⬝ᵥ xStar) + ↑(intermediateProgramDualPairing w wStar) = intermediateProgramBifunction data w0 x0 - ↑(x0 ⬝ᵥ xStar) + ↑(intermediateProgramDualPairing w0 wStar) + ↑(t * wStar.vStar i0)

Helper for Theorem 6.30.24: along the feasible ray obtained by increasing one threshold coordinate vᵢ, the adjoint integrand is affine in the ray parameter with slope vᵢ*.

theorem helperForTheorem_6_30_24_adjoint_eq_bot_of_exists_negativeMultiplier {m n n0 : ℕ} {ni : Fin m → ℕ} (data : IntermediateProgramData m n n0 ni) (hh0 : IsClosedProperConvexERealFunction data.h0) (hh : ∀ (i : Fin m), IsClosedProperConvexERealFunction (data.h i)) (xStar : Fin n → ℝ) (wStar : IntermediateProgramDualParameter m n n0 ni) (hneg : ∃ (i0 : Fin m), wStar.vStar i0 < 0) : adjointOfIntermediateProgram data xStar wStar = ⊥

Helper for Theorem 6.30.24: if one multiplier coordinate is negative, then the intermediate adjoint value is -∞, obtained by sending the corresponding threshold variable to +∞ along a feasible ray while keeping the affine-shift coordinates fixed.

theorem helperForTheorem_6_30_24_adjoint_eq_bot_of_not_dualFeasible_and_balance {m n n0 : ℕ} {ni : Fin m → ℕ} (data : IntermediateProgramData m n n0 ni) (hh0 : IsClosedProperConvexERealFunction data.h0) (hh : ∀ (i : Fin m), IsClosedProperConvexERealFunction (data.h i)) (xStar : Fin n → ℝ) (wStar : IntermediateProgramDualParameter m n n0 ni) (hnotfeas : ¬intermediateProgramDualFeasible data xStar wStar) (hbalance : data.a0Star + ∑ i : Fin m, wStar.vStar i • data.aStar i + data.A0.transpose.mulVec wStar.p0 + ∑ i : Fin m, (data.A i).transpose.mulVec (wStar.p i) = xStar) : adjointOfIntermediateProgram data xStar wStar = ⊥

Helper for Theorem 6.30.24: if the affine balance equation already holds, then any failure of dual feasibility must come from a negative multiplier coordinate, so the adjoint is -∞.

theorem helperForTheorem_6_30_24_not_dualFeasible_iff_exists_negativeMultiplier_or_balanceMismatch {m n n0 : ℕ} {ni : Fin m → ℕ} (data : IntermediateProgramData m n n0 ni) (xStar : Fin n → ℝ) (wStar : IntermediateProgramDualParameter m n n0 ni) : ¬intermediateProgramDualFeasible data xStar wStar ↔ (∃ (i : Fin m), wStar.vStar i < 0) ∨ (∀ (i : Fin m), 0 ≤ wStar.vStar i) ∧ data.a0Star + ∑ i : Fin m, wStar.vStar i • data.aStar i + data.A0.transpose.mulVec wStar.p0 + ∑ i : Fin m, (data.A i).transpose.mulVec (wStar.p i) ≠ xStar

Helper for Theorem 6.30.24: non-feasibility splits into the two structural obstruction branches that remain in the corrected proof plan, namely a negative multiplier or a failed balance equation under nonnegative multipliers.

@[reducible, inline]

abbrev helperForTheorem_6_30_24_negativeSignUniversalStatementProp : Prop

Helper for Theorem 6.30.24: the exact universal proposition obtained by abstracting the current negative-sign theorem header over the datum data and the convexity hypotheses.

@[reducible, inline]

abbrev helperForTheorem_6_30_24_positiveSignUniversalStatementProp : Prop

Helper for Theorem 6.30.24: the sign-only repaired universal proposition replaces the negative feasible-branch value by the positive-sign dual objective, but leaves the rest of the theorem unchanged.

theorem helperForTheorem_6_30_24_bothUniversalStatementTypes_not_nonempty : ¬Nonempty helperForTheorem_6_30_24_negativeSignUniversalStatementProp ∧ ¬Nonempty helperForTheorem_6_30_24_positiveSignUniversalStatementProp

Helper for Theorem 6.30.24: both universal theorem types are globally obstructed. The wrong-sign witness kills the literal current header, and the restricted-domain zero-multiplier witness kills the sign-only positive-sign repair.

theorem helperForTheorem_6_30_24_bothUniversalStatementTypes_isEmpty : IsEmpty helperForTheorem_6_30_24_negativeSignUniversalStatementProp ∧ IsEmpty helperForTheorem_6_30_24_positiveSignUniversalStatementProp

Helper for Theorem 6.30.24: both abstracted universal propositions are empty as types. This repackages the two ¬ Nonempty obstructions into the exact IsEmpty form needed to record that no proof term can exist for either the literal theorem header or the sign-only repair.

theorem helperForTheorem_6_30_24_constraint_lt_top_of_fullDomain {m n n0 : ℕ} {ni : Fin m → ℕ} (data : IntermediateProgramData m n n0 ni) {i : Fin m} {y : Fin (ni i) → ℝ} (hdomi : effectiveDomain Set.univ (data.h i) = Set.univ) : data.h i y < ⊤

Helper for Theorem 6.30.24: the full-domain hypothesis makes every constraint value finite above at every point.

@[reducible, inline]

abbrev helperForTheorem_6_30_24_dualBalanceVector {m n n0 : ℕ} {ni : Fin m → ℕ} (data : IntermediateProgramData m n n0 ni) (wStar : IntermediateProgramDualParameter m n n0 ni) : Fin n → ℝ

Helper for Theorem 6.30.24: the balance vector appearing in the explicit feasibility constraint, namely a₀* + ∑ᵢ vᵢ* aᵢ* + A₀ᵀ p₀* + ∑ᵢ Aᵢᵀ pᵢ*.

theorem helperForTheorem_6_30_24_mulVec_dotProduct_eq_dotProduct_transposeMulVec {k n : ℕ} (A : Matrix (Fin k) (Fin n) ℝ) (x : Fin n → ℝ) (p : Fin k → ℝ) : A.mulVec x ⬝ᵥ p = x ⬝ᵥ A.transpose.mulVec p

Helper for Theorem 6.30.24: dotting a matrix image against a covector is the same as dotting the original vector against the transposed matrix image of that covector.

theorem helperForTheorem_6_30_24_headAffineTerms_collect {m n n0 : ℕ} {ni : Fin m → ℕ} (data : IntermediateProgramData m n n0 ni) (x : Fin n → ℝ) (p0Star : Fin n0 → ℝ) : (data.A0.mulVec x + data.a0) ⬝ᵥ p0Star + (data.a0Star ⬝ᵥ x + data.α0) = x ⬝ᵥ (data.a0Star + data.A0.transpose.mulVec p0Star) + (data.α0 + data.a0 ⬝ᵥ p0Star)

Helper for Theorem 6.30.24: the head affine terms collect into the displayed coefficient of x plus the head constant term.

theorem helperForTheorem_6_30_24_constraintAffineTerms_collect {m n n0 : ℕ} {ni : Fin m → ℕ} (data : IntermediateProgramData m n n0 ni) (i : Fin m) (x : Fin n → ℝ) (lam : ℝ) (pStar : Fin (ni i) → ℝ) : ((data.A i).mulVec x + data.a i) ⬝ᵥ pStar + lam * (data.aStar i ⬝ᵥ x + data.α i) = x ⬝ᵥ (lam • data.aStar i + (data.A i).transpose.mulVec pStar) + (data.α i * lam + data.a i ⬝ᵥ pStar)

Helper for Theorem 6.30.24: for a fixed constraint index, the affine terms produced by the translated block collapse collect into the displayed linear coefficient of x plus the indexed constant term.

theorem helperForTheorem_6_30_24_iInf_parameter_eq_nestedBlocks {m n n0 : ℕ} {ni : Fin m → ℕ} (H : IntermediateProgramParameter m n n0 ni → EReal) : ⨅ (w : IntermediateProgramParameter m n n0 ni), H w = ⨅ (v : Fin m → ℝ), ⨅ (p0 : Fin n0 → ℝ), ⨅ (p : (i : Fin m) → Fin (ni i) → ℝ), H { v := v, p0 := p0, p := p }

Helper for Theorem 6.30.24: an infimum over intermediate-program perturbation parameters can be rewritten as nested infima over the scalar thresholds, the head translation p₀, and the dependent family of translated constraint coordinates pᵢ.

theorem helperForTheorem_6_30_24_feasibleIndicator_eq_sum_pairIndicators {m n n0 : ℕ} {ni : Fin m → ℕ} (data : IntermediateProgramData m n n0 ni) (x : Fin n → ℝ) (v : Fin m → ℝ) (p0 : Fin n0 → ℝ) (p : (i : Fin m) → Fin (ni i) → ℝ) : indicatorFunction (intermediateProgramFeasibleSet data { v := v, p0 := p0, p := p }) x = ∑ i : Fin m, if data.h i ((data.A i).mulVec x + data.a i - p i) + ↑(data.aStar i ⬝ᵥ x + data.α i) ≤ ↑(v i) then 0 else ⊤

Helper for Theorem 6.30.24: at fixed x, the feasibility indicator of the intermediate program splits into the finite sum of the independent scalar-threshold indicators for each pair (vᵢ, pᵢ).

theorem helperForTheorem_6_30_24_dependentFamily_iInf_sum_eq_sum_iInf_generic {m : ℕ} {α : Fin m → Type u_1} (g : (i : Fin m) → α i → EReal) (hfinite : ∀ (i : Fin m), ∃ (a : α i), g i a < ⊤) : ⨅ (z : (i : Fin m) → α i), ∑ i : Fin m, g i (z i) = ∑ i : Fin m, ⨅ (a : α i), g i a

Helper for Theorem 6.30.24: a dependent finite family of independent blocks splits under an infimum into the sum of the blockwise infima once each block has one finite witness.

theorem helperForTheorem_6_30_24_translationLinearTerms_collect {m n n0 : ℕ} {ni : Fin m → ℕ} (data : IntermediateProgramData m n n0 ni) (x xStar : Fin n → ℝ) (wStar : IntermediateProgramDualParameter m n n0 ni) : ↑(x ⬝ᵥ (data.a0Star + data.A0.transpose.mulVec wStar.p0)) + ∑ i : Fin m, ↑(x ⬝ᵥ (wStar.vStar i • data.aStar i + (data.A i).transpose.mulVec (wStar.p i))) + ↑(-(x ⬝ᵥ xStar)) = ↑(x ⬝ᵥ (helperForTheorem_6_30_24_dualBalanceVector data wStar - xStar))

Helper for Theorem 6.30.24: the linear terms coming from the head block, the indexed constraint blocks, and the outer subtraction -⟪x,x*⟫ collect into the single balance-vector coefficient a₀* + ∑ᵢ vᵢ* aᵢ* + A₀ᵀ p₀* + ∑ᵢ Aᵢᵀ pᵢ* - x*.

theorem helperForTheorem_6_30_24_headBlock_iInf_eq_linear_minus_fenchel {m n n0 : ℕ} {ni : Fin m → ℕ} (data : IntermediateProgramData m n n0 ni) (x : Fin n → ℝ) (wStar : IntermediateProgramDualParameter m n n0 ni) : ⨅ (p0 : Fin n0 → ℝ), data.h0 (data.A0.mulVec x + data.a0 - p0) + ↑(data.a0Star ⬝ᵥ x + data.α0) + ↑(p0 ⬝ᵥ wStar.p0) = ↑(x ⬝ᵥ (data.a0Star + data.A0.transpose.mulVec wStar.p0)) + (↑data.α0 + ↑(data.a0 ⬝ᵥ wStar.p0) - fenchelConjugate n0 data.h0 wStar.p0)

Helper for Theorem 6.30.24: after fixing the primal point x, the head p₀-block collapses to the expected affine term ⟪x, a₀* + A₀ᵀ p₀*⟫ plus the head contribution to the explicit dual objective.