Theorem 8.4A — a basic lift-and-project cut equals a simple disjunctive cut
ProvedDisjunctive.CutCorrespondence.lp_cut_eq_simple_disj_cutThis is Theorem 8.4A of Balas's Disjunctive Programming, cited to [33] — labeled
"Theorem 8.4" by statements.jsonl's regex extraction (the leading "8.4" and the letter "A"
were split by the extractor); corrected to "8.4A" here, matching the book's own two-part
"8.4A"/"8.4B" numbering (the only such split-lettered pair in the book).
The lift-and-project cut αx≥β from a basic feasible solution of (CGLP)_k (with u0,v0>0,
α,β basic, basic u/v indexed by M1,M2) is equivalent, as a set of x, to the simple
disjunctive cut from x_k≤0 ∨ x_k≥1 applied to the tableau row for x_k at J:=M1∪M2. The
book's proof exhibits the explicit correspondence (8.9): θα=πÂ, θβ=π0+πb̂, θu_J=π-π¹, θv_J=π-π², θu0=1-ā_k0, θv0=ā_k0 for a normalizing θ>0, and verifies it satisfies (8.2), then substitutes
(8.4) to recover π^s_J≥π0 from θαx≥θβ.
Formalization Note. Stated as a genuine set equality in x-space (not merely a formula
correspondence between coefficients), matching BRIEF.md's explicit warning against rephrasing
the equivalence away as an existential.
import Mathlib import Definitions.Def_Disjunctive_CutCorrespondence_Cglp import Definitions.Def_Disjunctive_CutCorrespondence_Tableau
namespace Disjunctive.CutCorrespondence
/-- Theorem 8.4A (Balas §8.1, p. 100, [33]): the lift-and-project cut `αx ≥ β` associated with a
basic feasible solution of `(CGLP)_k` (with `u0,v0>0`, `α,β` basic, and the basic `u`/`v`
components indexed by `M1`/`M2`) is equivalent, as a subset of `x`-space, to the simple
disjunctive cut from the disjunction `x_k ≤ 0 ∨ x_k ≥ 1` applied to the tableau row for `x_k`
defined by `J := M1 ∪ M2`. The solution is **basic**, not merely feasible with the given supports: support containment alone is false (one row `x ≥ 1/2` in `n = 1` with `u = 0.3`, `v = 0.1`, `u₀ = v₀ = 0.1` satisfies the hypotheses, `M1`/`M2` are not disjoint and Theorem 8.4A yields `x ≥ 3/4` instead of `x ≥ 1`). -/
theorem lp_cut_eq_simple_disj_cut {n : ℕ} {M : Type*} [Fintype M] [DecidableEq M]
[DecidableEq (Fin n)] (Atil : Matrix M (Fin n) ℝ) (btil : M → ℝ) (k : Fin n)
(α : Fin n → ℝ) (u : M → ℝ) (u0 : ℝ) (v : M → ℝ) (v0 : ℝ) (β : ℝ) (M1 M2 : Finset M)
(ι : Fin n → M) (hbasic : IsBasicCGLPKSolution Atil btil k α u u0 v v0 β) (hu0 : 0 < u0)
(hv0 : 0 < v0) (hu_supp : ∀ ρ ∉ M1, u ρ = 0) (hv_supp : ∀ ρ ∉ M2, v ρ = 0)
(hι_inj : Function.Injective ι) (hι_image : Finset.image ι Finset.univ = M1 ∪ M2)
(hnonsing : IsUnit (Ahat Atil ι).det) :
{x | β ≤ dotProduct α x} = SimpleDisjCutSet Atil btil ι k := by sorry
end Disjunctive.CutCorrespondence
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.