Prove2Me
Navigate
DiscoverFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

The fractional optimum is at most the integral optimum

Proved
PrimalDualOnline.SetCover.optFractional_le_optIntegral

by moutei · Sep 17, 2026 · Mathlib 0df444a (Lean v4.33.1)

approximation-algorithmscombinatoricsprimal-dualset-cover

If vfv_fvf​ is the least achievable fractional cover cost and viv_ivi​ is the least achievable integral cover cost for a set-cover instance, then

vf ≤ vi.v_f \ \le\ v_i.vf​ ≤ vi​.

The LP relaxation is a relaxation: every integral cover gives a fractional cover of the same cost via its indicator vector, so the fractional optimum can only be smaller. Both hypotheses are attainment statements, so each in particular asserts that the corresponding optimum exists; for an instance where either feasible set is empty the claim is vacuous. Nothing is asserted about the size of the integrality gap.

Instance-bundled hypotheses. The problem's two standing assumptions - every set cost is nonnegative, and every element lies in at least one available set - are not loose hypotheses of this statement. They are fields of the SetCoverInstance argument, so the statement cannot be instantiated at data violating either.

Preamble
import Definitions.Def_PrimalDualOnline_SetCover
import Mathlib.Tactic
Formal statement
open PrimalDualOnline.SetCover

theorem PrimalDualOnline.SetCover.optFractional_le_optIntegral
    {E S : Type*} [Fintype E] [Fintype S] [DecidableEq E] [DecidableEq S]
    (I : SetCoverInstance E S) (vf vi : ℝ)
    (hf : IsOptFractional I.sets I.cost vf) (hi : IsOptIntegral I.sets I.cost vi) :
    vf ≤ vi := by sorry
Source
Niv Buchbinder, Designing Competitive Online Algorithms via a Primal-Dual Approach, PhD thesis, Tel Aviv University, 2008, https://www.tau.ac.il/~nivb/download/phd-thsis.pdf, Section 2.2, the LP relaxation of program (P), p. 10
Read-back

What the Lean code literally says, in plain math · claude-opus-5

Read-backs: attainment and comparison of optimal cover values

Throughout, the following notation is used for the objects the three statements refer to. EEE and SSS are two types (indices for elements and for sets, respectively), each carrying a finiteness assumption. For s∈Ss \in Ss∈S we write As⊆EA_s \subseteq EAs​⊆E for the finite subset of EEE named by the first field of the bundled argument, and c(s)∈Rc(s) \in \mathbb{R}c(s)∈R for the real number named by its second field. For e∈Ee \in Ee∈E we write

cont(e)  =  { s∈S  :  e∈As },\mathrm{cont}(e) \;=\; \{\, s \in S \;:\; e \in A_s \,\},cont(e)={s∈S:e∈As​},

the (finite) set of indices whose set contains eee.

A cover is a finite subset C⊆SC \subseteq SC⊆S such that every e∈Ee \in Ee∈E satisfies e∈Ase \in A_se∈As​ for at least one s∈Cs \in Cs∈C; its cost is ∑s∈Cc(s)\sum_{s \in C} c(s)∑s∈C​c(s), each member of CCC counted once.

A fractional cover is an arbitrary real-valued function x:S→Rx : S \to \mathbb{R}x:S→R satisfying both

x(s)≥0  for every s∈S,∑s∈cont(e)x(s) ≥ 1  for every e∈E;x(s) \ge 0 \ \ \text{for every } s \in S, \qquad \sum_{s \in \mathrm{cont}(e)} x(s) \ \ge\ 1 \ \ \text{for every } e \in E;x(s)≥0  for every s∈S,s∈cont(e)∑​x(s) ≥ 1  for every e∈E;

its cost is ∑s∈Sc(s) x(s)\sum_{s \in S} c(s)\, x(s)∑s∈S​c(s)x(s), summed over all of SSS, not merely over the support of xxx.


PrimalDualOnline.SetCover.optFractional_le_optIntegral

Binders, instances and hypotheses. Implicitly given types EEE and SSS in arbitrary universes; four typeclass instances (EEE finite, SSS finite, equality on EEE decidable, equality on SSS decidable); one explicit bundled set-cover instance III over EEE and SSS, carrying the family A:S→A : S \toA:S→ (finite subsets of EEE), the cost c:S→Rc : S \to \mathbb{R}c:S→R, a proof that 0≤c(s)0 \le c(s)0≤c(s) for every s∈Ss \in Ss∈S, and a proof that every e∈Ee \in Ee∈E lies in AsA_sAs​ for at least one s∈Ss \in Ss∈S. Then two explicit real variables vfv_fvf​ and viv_ivi​, universally quantified, and two explicit hypotheses about them, stated for the same AAA and ccc drawn from III:

  • hfh_fhf​: vfv_fvf​ is the least element of the set of fractional cover costs, i.e. both
    • there exists x0:S→Rx_0 : S \to \mathbb{R}x0​:S→R with x0(s)≥0x_0(s) \ge 0x0​(s)≥0 for all sss, with ∑s∈cont(e)x0(s)≥1\sum_{s \in \mathrm{cont}(e)} x_0(s) \ge 1∑s∈cont(e)​x0​(s)≥1 for all e∈Ee \in Ee∈E, and with ∑s∈Sc(s) x0(s)=vf\sum_{s \in S} c(s)\,x_0(s) = v_f∑s∈S​c(s)x0​(s)=vf​; and
    • for every x:S→Rx : S \to \mathbb{R}x:S→R satisfying x(s)≥0x(s) \ge 0x(s)≥0 for all sss and ∑s∈cont(e)x(s)≥1\sum_{s \in \mathrm{cont}(e)} x(s) \ge 1∑s∈cont(e)​x(s)≥1 for all e∈Ee \in Ee∈E, one has vf≤∑s∈Sc(s) x(s)v_f \le \sum_{s \in S} c(s)\,x(s)vf​≤∑s∈S​c(s)x(s).
  • hih_ihi​: viv_ivi​ is the least element of the set of integral cover costs, i.e. both
    • there exists a finite C0⊆SC_0 \subseteq SC0​⊆S such that every e∈Ee \in Ee∈E lies in AsA_sAs​ for some s∈C0s \in C_0s∈C0​, and ∑s∈C0c(s)=vi\sum_{s \in C_0} c(s) = v_i∑s∈C0​​c(s)=vi​; and
    • for every finite C⊆SC \subseteq SC⊆S such that every e∈Ee \in Ee∈E lies in AsA_sAs​ for some s∈Cs \in Cs∈C, one has vi≤∑s∈Cc(s)v_i \le \sum_{s \in C} c(s)vi​≤∑s∈C​c(s).

The conclusion.

vf  ≤  vi.v_f \;\le\; v_i .vf​≤vi​.

That is: for any two reals standing in those two least-element relations with respect to one and the same family AAA and cost ccc, the fractional value is less than or equal to the integral value. The inequality is non-strict, in that direction: fractional on the left, integral on the right.

1. Attainment vs. infimum vs. boundedness. This statement does not itself assert that any minimum is attained; attainment appears here only inside its hypotheses. Each of hfh_fhf​ and hih_ihi​ is a least-element assumption, and each accordingly contains an attainment clause (a witness x0x_0x0​, respectively C0C_0C0​, realizing the value) alongside a lower-bound clause. The conclusion is a plain comparison of two given reals. So the logical shape is: if both minima are attained at the values vfv_fvf​ and viv_ivi​, then vf≤viv_f \le v_ivf​≤vi​. Nothing asserts that such vfv_fvf​ or viv_ivi​ exist; if for some instance no such pair existed, the statement would hold vacuously for that instance.

2. Provenance and load-bearing status of the two side conditions.

  • Nonnegativity of cost is present, as field 3 of the bundled argument III — not as a loose hypothesis, and not restated in hfh_fhf​ or hih_ihi​. As regards the conclusion it does no work: the hypothesis hfh_fhf​ already supplies a lower-bound clause quantified over all feasible xxx, and hih_ihi​ already supplies a witness cover, so the comparison follows from the hypotheses without reference to the signs of the c(s)c(s)c(s). What dropping nonnegativity would change is the population of instances to which the statement applies: with some c(s0)<0c(s_0) < 0c(s0​)<0 the fractional cost can be driven to −∞-\infty−∞ along increasing x(s0)x(s_0)x(s0​) (raising one coordinate preserves nonnegativity and every covering constraint), so the lower-bound clause of hfh_fhf​ would be unsatisfiable and the hypothesis hfh_fhf​ could hold for no vfv_fvf​ at all. The implication would then be vacuous rather than false.
  • Every element lies in some set (coverability) is present, as field 4 of the bundled argument III. It likewise does no work in deriving the conclusion, since the membership clauses of hfh_fhf​ and hih_ihi​ already assert that a feasible x0x_0x0​ and a cover C0C_0C0​ exist. If it were dropped and some e0e_0e0​ were in no AsA_sAs​, then cont(e0)=∅\mathrm{cont}(e_0) = \emptysetcont(e0​)=∅ and its constraint 0≥10 \ge 10≥1 is unsatisfiable, and no finite CCC covers e0e_0e0​; both membership clauses would fail, so neither hfh_fhf​ nor hih_ihi​ could be satisfied, and the statement would again be vacuously true rather than false. In short: in this statement both bundled conditions bear on whether the hypotheses are satisfiable, not on the conclusion.

3. Can either extremal set be empty? Two readings, both addressed.

  • The two value sets. Under the hypotheses, neither can be empty. The membership clause of hfh_fhf​ places vfv_fvf​ in the set of fractional cover costs, and the membership clause of hih_ihi​ places viv_ivi​ in the set of integral cover costs; a set with a least element is nonempty by definition. If one of them could be empty for a given instance, the corresponding hypothesis would be unsatisfiable and the statement would carry no content for that instance — it would be vacuously true, asserting nothing about vfv_fvf​ and viv_ivi​. (Coverability, as noted above, is the bundled condition that rules this out independently of the hypotheses, except in the vacuous case EEE empty where both sets contain 000.)
  • The extremal witnesses. The minimizing cover C0C_0C0​ furnished by hih_ihi​ can be the empty subset of SSS, but only when EEE is empty: the covering condition on C0=∅C_0 = \emptysetC0​=∅ requires, for each e∈Ee \in Ee∈E, some s∈∅s \in \emptysets∈∅ with e∈Ase \in A_se∈As​, which is impossible unless there is no eee. Likewise the minimizing x0x_0x0​ furnished by hfh_fhf​ can be the zero function only when EEE is empty, since otherwise each eee forces ∑s∈cont(e)x0(s)≥1>0\sum_{s \in \mathrm{cont}(e)} x_0(s) \ge 1 > 0∑s∈cont(e)​x0​(s)≥1>0. In that EEE-empty case vi=∑s∈∅c(s)=0v_i = \sum_{s \in \emptyset} c(s) = 0vi​=∑s∈∅​c(s)=0 and vf=0v_f = 0vf​=0, and the asserted inequality reads 0≤00 \le 00≤0, which holds as an equality. So the empty-witness case does not contradict the conclusion; it is one of the cases in which the conclusion is an equality rather than a strict inequality. Separately, C0C_0C0​ may be nonempty yet contain sets that contribute nothing (see item 5), since the covering condition never demands minimality.

4. Hypotheses relative to the two existence statements. All three statements share the identical prefix: the same two implicit types, the same four typeclass instances (EEE finite, SSS finite, equality decidable on EEE, equality decidable on SSS), and the same single explicit bundled set-cover instance III with its four fields. Neither existence statement carries any hypothesis that this comparison statement lacks. This statement carries strictly more: two additional explicit real arguments vf,viv_f, v_ivf​,vi​, and two additional explicit hypotheses hf,hih_f, h_ihf​,hi​ asserting that each is the least element of its respective value set. It does not assume the two existence theorems as such; it takes the two least elements as given data and hypotheses. Conversely, the existence statements assume nothing about any value, about the other notion of cover, or about a relationship between them.

5. Degenerate cases silently included.

  • EEE empty. Both feasibility notions become vacuous: every finite C⊆SC \subseteq SC⊆S is a cover and every nonnegative xxx is a fractional cover. With nonnegative costs the least values are vi=0v_i = 0vi​=0 (attained at C0=∅C_0 = \emptysetC0​=∅) and vf=0v_f = 0vf​=0 (attained at x0≡0x_0 \equiv 0x0​≡0), and the conclusion holds with equality. Coverability is vacuously satisfiable, so such bundled instances exist for any AAA and any nonnegative ccc.
  • SSS empty. Coverability requires some s∈Ss \in Ss∈S for each e∈Ee \in Ee∈E, so an instance with SSS empty forces EEE empty. Then the only finite subset of SSS is ∅\emptyset∅ and the only function S→RS \to \mathbb{R}S→R is the empty function; both value sets are {0}\{0\}{0}, so vf=vi=0v_f = v_i = 0vf​=vi​=0 and the conclusion is 0≤00 \le 00≤0.
  • c≡0c \equiv 0c≡0. Nonnegativity holds; every cover and every fractional cover has cost 000, so the hypotheses force vf=vi=0v_f = v_i = 0vf​=vi​=0 and the asserted inequality is an equality. The statement's non-strict ≤\le≤ admits this.
  • Individual zero-cost sets. Sets sss with c(s)=0c(s) = 0c(s)=0 may be added to a minimizing cover C0C_0C0​, or given arbitrary nonnegative mass x0(s)x_0(s)x0​(s), without changing either cost. Hence neither extremal witness is pinned down by the hypotheses, and C0C_0C0​ need not be inclusion-minimal or of minimum cardinality. The values vfv_fvf​ and viv_ivi​ are nonetheless each fixed by their hypothesis, since a subset of R\mathbb{R}R has at most one least element — though the statement asserts only the inequality between them, not this or any uniqueness.
  • Unbounded entries of a fractional cover. The lower-bound clause of hfh_fhf​ is quantified over all nonnegative xxx meeting the covering constraints, with no upper bound on any x(s)x(s)x(s), no x(s)≤1x(s) \le 1x(s)≤1, no integrality and no rationality; entries may be arbitrarily large reals. Such xxx are therefore included in the comparison range of hfh_fhf​, and the set of fractional costs is in general unbounded above; this does not affect the conclusion, which concerns only the least elements. The attaining x0x_0x0​ is likewise unconstrained in magnitude.

What is NOT asserted. The statement does not assert that vfv_fvf​ or viv_ivi​ exists — only what follows if both are given. It does not assert equality, nor strictness, nor any gap or ratio bound in the other direction: there is no claim of the form vi≤α vfv_i \le \alpha\, v_fvi​≤αvf​ for any α\alphaα, no integrality-gap bound, no claim about max⁡e∣cont(e)∣\max_e |\mathrm{cont}(e)|maxe​∣cont(e)∣ or any frequency- or logarithm-based factor. It does not claim that vfv_fvf​ and viv_ivi​ are unique (that a set has at most one least element is not part of what is asserted), nor that either is nonnegative, nonzero, rational or finite in any sense beyond being real. It says nothing about the relationship between the attaining witnesses x0x_0x0​ and C0C_0C0​ — in particular nothing about rounding a fractional cover to a cover, nothing about indicator functions of covers, and nothing about supports. It makes no duality claim: nothing about dual packings, ∑ey(e)\sum_e y(e)∑e​y(e), weak duality or complementary slackness. And it makes no algorithmic, greedy, primal-dual, online or complexity claim.

Human review
  • Endorsed by Shuze Chen · Sep 17, 2026

  • Endorsed by moutei · Sep 17, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me