noncomputable def classicalDecidablePredPart9 {α : Type u_1} (p : α → Prop) : DecidablePred p

Predicates on coordinate spaces in this section are treated classically when needed in piecewise definitions.

theorem helperForText_34_1_4_rawMixedClosureOrder_missingPrerequisite {m n : ℕ} (K : SaddleFunction m n) (h : IsConcaveConvex K) (hOrder : lowerClosureConcaveConvex K h ≤ upperClosureConcaveConvex K h) : partialClosure₂ (partialClosure₁ K) ≤ partialClosure₁ (partialClosure₂ K)

Helper for Text 34.1.4: after checking both the local-minimax route and the Section 33 uniqueness route, the unresolved dependency-closed blocker is exactly the original-text bridge cl₂ overline(K) = underline(K), from which the normalized raw mixed-order comparison follows formally.

theorem helperForText_34_1_4_reverseMinimax_bridge {m n : ℕ} (K : SaddleFunction m n) (h : IsConcaveConvex K) (hOrder : lowerClosureConcaveConvex K h ≤ upperClosureConcaveConvex K h) : partialClosure₂ (partialClosure₁ K) ≤ partialClosure₁ (partialClosure₂ K)

Helper bridge for Text 34.1.4: the exact upstream reverse-minimax input needed by the proof pipeline is precisely the normalized raw mixed-order inequality cl₂ (cl₁ K) ≤ cl₁ (cl₂ K). This theorem is just the dependency-closed package of the existing missing-prerequisite lemma, exposed under the name the later endgame uses conceptually.

theorem helperForText_34_1_4_secondClosureOfUpper_eq_lower_from_concaveConvex {m n : ℕ} (K : SaddleFunction m n) (h : IsConcaveConvex K) (hNoBotK : HasNoBotValuesBifunction K) (hOrder : lowerClosureConcaveConvex K h ≤ upperClosureConcaveConvex K h) : partialClosure₂ (upperClosureConcaveConvex K h) = lowerClosureConcaveConvex K h

Helper for Text 34.1.4: once the normalized raw mixed-order comparison is supplied, the exact recovery cl₂ overline(K) = underline(K) follows formally from the already-proved local endgame.

theorem helperForText_34_1_4_mixedClosure_order {m n : ℕ} (K : SaddleFunction m n) (h : IsConcaveConvex K) (hOrder : lowerClosureConcaveConvex K h ≤ upperClosureConcaveConvex K h) : lowerClosureConcaveConvex K h ≤ upperClosureConcaveConvex K h

Helper for Text 34.1.4: the only remaining upstream prerequisite is now the mixed-order comparison underline(K) ≤ overline(K) for a bare concave-convex saddle-function.

theorem helperForText_34_1_4_secondClosureOfUpper_eq_lower {m n : ℕ} (K : SaddleFunction m n) (h : IsConcaveConvex K) (hNoBotK : HasNoBotValuesBifunction K) (hOrder : lowerClosureConcaveConvex K h ≤ upperClosureConcaveConvex K h) : partialClosure₂ (upperClosureConcaveConvex K h) = lowerClosureConcaveConvex K h

Helper for Text 34.1.4: after isolating the true upstream blocker to the mixed-order comparison, the exact recovery cl₂ overline(K) = underline(K) follows formally.

theorem helperForText_34_1_4_upperClosure_le_firstClosureOfLower {m n : ℕ} (K : SaddleFunction m n) (h : IsConcaveConvex K) : upperClosureConcaveConvex K h ≤ partialClosure₁ (lowerClosureConcaveConvex K h)

Helper for Text 34.1.4: independently of the unresolved mixed-order comparison, the mixed upper closure always lies below cl₁ of the mixed lower closure.

theorem helperForText_34_1_4_firstClosureOfLower_le_upper_of_mixedClosure_order {m n : ℕ} (K : SaddleFunction m n) (h : IsConcaveConvex K) (hNoBotK : HasNoBotValuesBifunction K) (hOrder : lowerClosureConcaveConvex K h ≤ upperClosureConcaveConvex K h) : partialClosure₁ (lowerClosureConcaveConvex K h) ≤ upperClosureConcaveConvex K h

Helper for Text 34.1.4: once the mixed lower closure is known to lie below the mixed upper closure, first-variable closedness of the upper closure gives the reverse cl₁ bound.

theorem helperForText_34_1_4_firstClosureOfLower_eq_upper_of_mixedClosure_order {m n : ℕ} (K : SaddleFunction m n) (h : IsConcaveConvex K) (hNoBotK : HasNoBotValuesBifunction K) (hOrder : lowerClosureConcaveConvex K h ≤ upperClosureConcaveConvex K h) : partialClosure₁ (lowerClosureConcaveConvex K h) = upperClosureConcaveConvex K h

Helper for Text 34.1.4: the mixed-order comparison already forces the first cross-closure identity cl₁ underline(K) = overline(K).

theorem helperForText_34_1_4_lowerClosure_le_secondClosureOfUpper_of_mixedClosure_order {m n : ℕ} (K : SaddleFunction m n) (h : IsConcaveConvex K) (hNoBotK : HasNoBotValuesBifunction K) (hOrder : lowerClosureConcaveConvex K h ≤ upperClosureConcaveConvex K h) : lowerClosureConcaveConvex K h ≤ partialClosure₂ (upperClosureConcaveConvex K h)

Helper for Text 34.1.4: once the mixed lower closure is known to lie below the mixed upper closure, second-variable closedness of the lower closure gives the reverse cl₂ bound.

theorem helperForText_34_1_4_concaveConvex_crossClosure_of_rawMixedClosureOrder {m n : ℕ} (K : SaddleFunction m n) (h : IsConcaveConvex K) (hNoBotK : HasNoBotValuesBifunction K) (hRawOrder : partialClosure₂ (partialClosure₁ K) ≤ partialClosure₁ (partialClosure₂ K)) : partialClosure₁ (lowerClosureConcaveConvex K h) = upperClosureConcaveConvex K h ∧ partialClosure₂ (upperClosureConcaveConvex K h) = lowerClosureConcaveConvex K h

Helper for Text 34.1.4: the raw mixed-order inequality on cl₂ (cl₁ K) and cl₁ (cl₂ K) already packages the full concave-convex cross-closure conclusion.

theorem helperForText_34_1_4_concaveConvex_crossClosure_of_secondClosure_eq_lower {m n : ℕ} (K : SaddleFunction m n) (h : IsConcaveConvex K) (hNoBotK : HasNoBotValuesBifunction K) (hRecover : partialClosure₂ (upperClosureConcaveConvex K h) = lowerClosureConcaveConvex K h) : partialClosure₁ (lowerClosureConcaveConvex K h) = upperClosureConcaveConvex K h ∧ partialClosure₂ (upperClosureConcaveConvex K h) = lowerClosureConcaveConvex K h

Helper for Text 34.1.4: once the exact recovery cl₂ overline(K) = underline(K) is known, both cross-closure identities follow immediately.

theorem helperForText_34_1_4_concaveConvex_crossClosure_iff_secondClosureOfUpper_eq_lower {m n : ℕ} (K : SaddleFunction m n) (h : IsConcaveConvex K) (hNoBotK : HasNoBotValuesBifunction K) : partialClosure₁ (lowerClosureConcaveConvex K h) = upperClosureConcaveConvex K h ∧ partialClosure₂ (upperClosureConcaveConvex K h) = lowerClosureConcaveConvex K h ↔ partialClosure₂ (upperClosureConcaveConvex K h) = lowerClosureConcaveConvex K h

Helper for Text 34.1.4: the full textbook pair of cross-closure identities is equivalent to the exact recovery statement cl₂ overline(K) = underline(K).

theorem helperForText_34_1_4_mixedClosure_order_of_firstClosure_eq_upper {m n : ℕ} (K : SaddleFunction m n) (h : IsConcaveConvex K) (hFirst : partialClosure₁ (lowerClosureConcaveConvex K h) = upperClosureConcaveConvex K h) : lowerClosureConcaveConvex K h ≤ upperClosureConcaveConvex K h

Helper for Text 34.1.4: the first cross-closure identity already forces the textbook mixed-order comparison.

theorem helperForText_34_1_4_mixedClosure_order_iff_crossClosure {m n : ℕ} (K : SaddleFunction m n) (h : IsConcaveConvex K) (hNoBotK : HasNoBotValuesBifunction K) : lowerClosureConcaveConvex K h ≤ upperClosureConcaveConvex K h ↔ partialClosure₁ (lowerClosureConcaveConvex K h) = upperClosureConcaveConvex K h ∧ partialClosure₂ (upperClosureConcaveConvex K h) = lowerClosureConcaveConvex K h

Helper for Text 34.1.4: the textbook mixed-order comparison is equivalent to the two cross-closure identities.

theorem helperForText_34_1_4_concaveConvex_crossClosure_iff_rawMixedClosureOrder {m n : ℕ} (K : SaddleFunction m n) (h : IsConcaveConvex K) (hNoBotK : HasNoBotValuesBifunction K) : partialClosure₁ (lowerClosureConcaveConvex K h) = upperClosureConcaveConvex K h ∧ partialClosure₂ (upperClosureConcaveConvex K h) = lowerClosureConcaveConvex K h ↔ partialClosure₂ (partialClosure₁ K) ≤ partialClosure₁ (partialClosure₂ K)

Helper for Text 34.1.4: the full concave-convex textbook conclusion is equivalent to the raw operator inequality cl₂ (cl₁ K) ≤ cl₁ (cl₂ K).

theorem helperForText_34_1_4_concaveConvex_crossClosure {m n : ℕ} (K : SaddleFunction m n) (h : IsConcaveConvex K) (hOrder : lowerClosureConcaveConvex K h ≤ upperClosureConcaveConvex K h) (hLowerClosed : IsConvexClosedInSecond (lowerClosureConcaveConvex K h)) (hUpperClosed : IsConcaveClosedInFirst (upperClosureConcaveConvex K h)) : partialClosure₁ (lowerClosureConcaveConvex K h) = upperClosureConcaveConvex K h ∧ partialClosure₂ (upperClosureConcaveConvex K h) = lowerClosureConcaveConvex K h

Helper for Text 34.1.4: after the lower recovery cl₂ overline(K) = underline(K) is known, the first cross-closure identity is the short textbook rewrite cl₁ underline(K) = cl₁ (cl₂ overline(K)) = overline(K).

theorem section34_text_34_1_4 {m n : ℕ} (K : SaddleFunction m n) (h : IsConcaveConvex K) (hOrder : lowerClosureConcaveConvex K h ≤ upperClosureConcaveConvex K h) (hLowerClosed : IsConvexClosedInSecond (lowerClosureConcaveConvex K h)) (hUpperClosed : IsConcaveClosedInFirst (upperClosureConcaveConvex K h)) : partialClosure₁ (lowerClosureConcaveConvex K h) = upperClosureConcaveConvex K h ∧ partialClosure₂ (upperClosureConcaveConvex K h) = lowerClosureConcaveConvex K h

Text 34.1.4, qualified formal version: if K is concave-convex, its mixed closures are ordered, and the outer closures are fixed in their respective variables, then applying the opposite partial closures exchanges the mixed pair.

theorem helperForText_34_0_1_crossClosure_relations_of_mixedClosure_order {m n : ℕ} (K : SaddleFunction m n) (h : IsConcaveConvex K) (hNoBotK : HasNoBotValuesBifunction K) (hOrder : lowerClosureConcaveConvex K h ≤ upperClosureConcaveConvex K h) : partialClosure₁ (lowerClosureConcaveConvex K h) = upperClosureConcaveConvex K h ∧ partialClosure₂ (upperClosureConcaveConvex K h) = lowerClosureConcaveConvex K h

Helper for Text 34.0.1: once the mixed lower closure is known to lie below the mixed upper closure, the two cross-closure identities follow from monotonicity and the one-sided fixed-point properties of the outer closures.

theorem helperForText_34_0_1_partialClosure₁_idempotent_unconditional {m n : ℕ} (K : SaddleFunction m n) : partialClosure₁ (partialClosure₁ K) = partialClosure₁ K

Helper for Text 34.0.1: the first partial closure is unconditionally idempotent.

theorem helperForText_34_0_1_partialClosure₁_idempotent {m n : ℕ} (K : SaddleFunction m n) (_h : IsConcaveConvex K) : partialClosure₁ (partialClosure₁ K) = partialClosure₁ K

Compatibility form of first-partial-closure idempotence for concave-convex kernels.

theorem helperForText_34_0_1_partialClosure₂_idempotent_unconditional {m n : ℕ} (K : SaddleFunction m n) : partialClosure₂ (partialClosure₂ K) = partialClosure₂ K

Helper for Text 34.0.1: the second partial closure is unconditionally idempotent.

theorem helperForText_34_0_1_partialClosure₂_idempotent {m n : ℕ} (K : SaddleFunction m n) (_h : IsConcaveConvex K) : partialClosure₂ (partialClosure₂ K) = partialClosure₂ K

Compatibility form of second-partial-closure idempotence for concave-convex kernels.

theorem helperForText_34_0_1_lower_and_upper_fixedPoint_forms {m n : ℕ} (K : SaddleFunction m n) (h : IsConcaveConvex K) : partialClosure₂ (partialClosure₁ (lowerClosureConcaveConvex K h)) = lowerClosureConcaveConvex K h ∧ partialClosure₁ (partialClosure₂ (upperClosureConcaveConvex K h)) = upperClosureConcaveConvex K h

Helper for Text 34.0.1: both mixed closures are fixed points of repeating the lower or upper closure operation.

theorem helperForText_34_0_1_lowerClosed_from_fixedPoint {m n : ℕ} (K : SaddleFunction m n) (h : IsConcaveConvex K) (hNoBotK : HasNoBotValuesBifunction K) (hFixed : partialClosure₂ (partialClosure₁ (lowerClosureConcaveConvex K h)) = lowerClosureConcaveConvex K h) : IsLowerClosed (lowerClosureConcaveConvex K h)

Helper for Text 34.0.1: a mixed lower closure is lower closed once the repeated lower closure operation fixes it.

theorem helperForText_34_0_1_upperClosed_from_fixedPoint {m n : ℕ} (K : SaddleFunction m n) (h : IsConcaveConvex K) (hNoBotK : HasNoBotValuesBifunction K) (hFixed : partialClosure₁ (partialClosure₂ (upperClosureConcaveConvex K h)) = upperClosureConcaveConvex K h) : IsUpperClosed (upperClosureConcaveConvex K h)

Helper for Text 34.0.1: an upper mixed closure is upper closed once the repeated upper closure operation fixes it.

theorem helperForText_34_0_1_packaged_closedness_conclusions {m n : ℕ} (K : SaddleFunction m n) (h : IsConcaveConvex K) (hNoBotK : HasNoBotValuesBifunction K) : IsLowerClosed (lowerClosureConcaveConvex K h) ∧ IsUpperClosed (upperClosureConcaveConvex K h)

Helper for Text 34.0.1: the fixed-point forms package directly into the lower-closed and upper-closed conclusions for the two mixed closures.

theorem helperForText_34_0_1_closedConvexWitness_exists_forces_main_conclusion {m n : ℕ} (K : SaddleFunction m n) (h : IsConcaveConvex K) (hNoBotK : HasNoBotValuesBifunction K) (hLowerNoTopBot : HasNoTopOrBotValuesBifunction (lowerClosureConcaveConvex K h)) (hWitness : ∃ (F : (Fin m → ℝ) → (Fin n → ℝ) → EReal), IsRockafellarConvexBifunction F ∧ HasNoBotValuesBifunction F ∧ ClosedConvexBifunction F ∧ lowerClosureConcaveConvex K h = convexBifunctionPairing F ∧ upperClosureConcaveConvex K h = helperForText_34_0_1_convexAdjointPairingKernel F) : partialClosure₂ (partialClosure₁ (partialClosure₂ (partialClosure₁ K))) = partialClosure₂ (partialClosure₁ K) ∧ partialClosure₁ (partialClosure₂ (partialClosure₁ (partialClosure₂ K))) = partialClosure₁ (partialClosure₂ K) ∧ IsLowerClosed (lowerClosureConcaveConvex K h) ∧ IsUpperClosed (upperClosureConcaveConvex K h)

Helper for Text 34.0.1: once the normalized existential witness is available, the full idempotence and lower/upper closedness conclusion follows by the local closure chain already established in this file.

theorem section34_idempotent_closures {m n : ℕ} (K : SaddleFunction m n) (h : IsConcaveConvex K) (hNoBotK : HasNoBotValuesBifunction K) : partialClosure₂ (partialClosure₁ (partialClosure₂ (partialClosure₁ K))) = partialClosure₂ (partialClosure₁ K) ∧ partialClosure₁ (partialClosure₂ (partialClosure₁ (partialClosure₂ K))) = partialClosure₁ (partialClosure₂ K) ∧ IsLowerClosed (lowerClosureConcaveConvex K h) ∧ IsUpperClosed (upperClosureConcaveConvex K h)

Text 34.0.1: for a concave-convex saddle-function, the iterated lower and upper closure operations are idempotent, and consequently the lower closure is lower closed while the upper closure is upper closed.

theorem section34_lower_and_upper_closures_are_closed {m n : ℕ} (K : SaddleFunction m n) (h : IsConcaveConvex K) (hNoBotK : HasNoBotValuesBifunction K) : IsLowerClosed (lowerClosureConcaveConvex K h) ∧ IsUpperClosed (upperClosureConcaveConvex K h)

Theorem 34.1: if K is any saddle-function on ℝ^m × ℝ^n, then its lower closure is a lower closed saddle-function and its upper closure is an upper closed saddle-function.