The optimal bound for a fixed number of variables

Statement

For every n ≥ 1, the optimal universal lower bound for $\mathbb P(S<\mathbb ES+1)$ is $\left(\frac n{n+1}\right)^n$ , over independent nonnegative integrable X₁,…,Xₙ with E Xᵢ ≤ 1.

Assumptions

Fix positive finite n.
Strict unit-slack event and individual means at most one.

Scope

Both July arguments support the same mathematical assertion. The pinned Lean declaration formalizes this fixed-dimensional optimality statement.

Explanation

Proof outlines · 2

Fu–Han–Wang–Yan–Zhang–Zhou account

Sharp small-deviation inequalities

This account gives the sharp finite-dimensional unit-slack constant and a broader deviation inequality.

Its general deviation bound is sharp on the δ ≥ 1 branch; the later all-δ proposal is assessed separately.

Proved: Sharp unit-slack bound proved by Fu and coauthors ↗ · source dated Jul 27, 2026 · observed Oct 13, 2026. Theorem 1.1 at δ = 1, including finite-dimensional sharpness.

Independent mathematical assessment of this argument remains separate from the statement’s attributed status.

The optimal bound for a fixed number of variables →

Sharp small-deviation inequalities for sums of independent nonnegative random variables →

Nie–Wei account

A separate sharp-bound argument

A second author team establishes the same sharp finite-dimensional unit-slack constant.

The Wang–Zhang formal project has its own scope; credit for this mathematical argument remains separate.

Proved: Unit-slack bound proved by Nie and Wei ↗ · source dated Jul 27, 2026 · observed Oct 13, 2026. Their separately authored proof reaches the same finite-dimensional constant.

Independent mathematical assessment of this argument remains separate from the statement’s attributed status.

The optimal bound for a fixed number of variables →

On Feige’s conjecture →

Constructions · 1

A finite-dimensional extremizer

Distribution: Independent Xᵢ: value 0 with probability n/(n+1), and value n+1 with probability 1/(n+1).
Mean: Each mean is one; E S = n.
Strict event: S < n+1 occurs exactly when every variable is zero, with probability (n/(n+1))^n.

This attains the fixed-n bound. The dimension-free constant 1/e is approached as n grows and is not attained by this family at finite n.

The optimal bound for a fixed number of variables →

Bounds & computations · 1

Compare the quantity and hypotheses within each group. A finite check, conditional theorem and proposed improvement cover different scopes.

Unit-slack probability
Result	Value	Conditions
The optimal bound for a fixed number of variables → Proved Selected source date: Jul 27, 2026	(n/(n+1))ⁿ	Optimal lower bound for fixed finite n; tends to 1/e without attaining it at finite n. Sharp small-deviation inequalities for sums of independent nonnegative random variables → On Feige’s conjecture → Lean proof of the sharp unit-slack Feige bound →

Evidence

Source reports

Proved

Unit-slack bound proved by Nie and Wei ↗

Their separately authored proof reaches the same finite-dimensional constant.

On Feige’s conjecture · Theorem 1.3 and AI acknowledgement; arXiv submitted 27 July, HTML manuscript dated 24 August →

Source dated Jul 27, 2026 · Observed Oct 13, 2026

Proved

Unit-slack optimality reported complete in Lean ↗

The pinned source targets δ = 1 only; no general-δ formal proof is attributed to it.

Lean proof of the sharp unit-slack Feige bound · PalomarFeige.sharp_unit_slack_feige_complete; README and formalization metadata →

Observed Oct 13, 2026

Proved

Sharp unit-slack bound proved by Fu and coauthors ↗

Theorem 1.1 at δ = 1, including finite-dimensional sharpness.

Sharp small-deviation inequalities for sums of independent nonnegative random variables · Theorem 1.1, Corollary 1.2 and AI disclosure →

Source dated Jul 27, 2026 · Observed Oct 13, 2026

Formal proofs

Sharp finite-dimensional Feige inequality ↗

Complete formal proof reported externally

Lean 4 proof reports complete fixed-n optimality for δ = 1. It does not certify the July δ-dependent theorem or Ling’s Samuels proposal. Source definitions quantify over measurable, integrable, pointwise nonnegative independent variables on probability spaces.

Statement match: Linked by OpenMath · independent review separate · checked Oct 13, 2026

Declaration & revision

PalomarFeige.sharp_unit_slack_feige_complete

Commit 19c61d6cb556d1e967dbb0ada9f293c290837867

Lean proof of the sharp unit-slack Feige bound: PalomarFeige.sharp_unit_slack_feige_complete; README and formalization metadata →

Connections

In this problem · publication v7

Feige’s probability conjecture →

Bound · Proved

Related statements

This statement: The optimal bound for a fixed number of variables

The finite constants (n/(n+1))^n decrease to 1/e; each is strictly larger than 1/e.

Finite-n sharpness and the limiting universal bound are not identical statements.

Details & sources

The optimal bound for a fixed number of variables →

Proved · version 1

For every n ≥ 1, the optimal universal lower bound for $\mathbb P(S<\mathbb ES+1)$ is $\left(\frac n{n+1}\right)^n$ , over independent nonnegative integrable X₁,…,Xₙ with E Xᵢ ≤ 1.

Fix positive finite n.
Strict unit-slack event and individual means at most one.

Scope: Both July arguments support the same mathematical assertion. The pinned Lean declaration formalizes this fixed-dimensional optimality statement.

The dimension-free unit-slack inequality →

Proved · version 1

For every n ≥ 1 and independent nonnegative integrable X₁,…,Xₙ with E Xᵢ ≤ 1, $\mathbb P(S<\mathbb ES+1)\ge e^{-1}$ , where $S=\sum_i X_i$ .

Positive finite number of independent variables.
Nonnegative variables with each mean at most one; strict threshold.

Scope: The conventional unit-slack conjecture. The stronger finite-n theorem yields this bound and approaches 1/e as n grows.

Relationship not independently reviewed.

Connection in Feige’s probability conjecture →

Relationship not independently reviewed. This concerns its use in this problem.

Sources

Lean proof of the sharp unit-slack Feige bound →

PalomarFeige.sharp_unit_slack_feige_complete; README and formalization metadata → · Original passage ↗
Recorded wording
The headline theorem asserts optimality of (n/(n+1))^n for every positive finite n in the strict unit-slack event.
paraphrase · OpenMath supplies its own mathematical paraphrases and links; proof text is not republished.

Guanyang Wang · Peng Zhang · Project documentation

Public formal source; execution and statement correspondence are separate checks.

Lean proof of the sharp unit-slack Feige bound — pinned source ↗No OpenMath execution recorded

Exact source inspected; OpenMath has not executed this formal proof project.

Revision & attribution

Source revision: 19c61d6cb556d1e967dbb0ada9f293c290837867. Observed Oct 13, 2026.

The project credits GPT-5.6 Sol Codex for formalization. This is a different contribution from the July discovery model. Authors report verification; OpenMath has not executed it.

Lean proof of the sharp unit-slack Feige bound — pinned source: 19c61d6cb556d1e967dbb0ada9f293c290837867.

On Feige’s conjecture →

Theorem 1.3 and AI acknowledgement; arXiv submitted 27 July, HTML manuscript dated 24 August → · Original passage ↗
Recorded wording
Gives a separate argument for the unit-slack inequality and the bound δ(n/(n+δ))^n for 0 < δ ≤ 1 under unit means.
paraphrase · OpenMath supplies its own mathematical paraphrases and links; proof text is not republished.

Zipei Nie · Jiaye Wei · Preprint · Publication date Jul 27, 2026

Revision & attribution

Source revision: 2026-07-27. Observed Oct 13, 2026.

Nie and Wei credit GPT-5.6 Sol for exploration and discovery, state that they checked the arguments and authored the text, and retain responsibility. Their argument uses the Vlassis–Thomas calibration theorem.

Sharp small-deviation inequalities for sums of independent nonnegative random variables →

Theorem 1.1, Corollary 1.2 and AI disclosure → · Original passage ↗
Recorded wording
Proves two parameter-range lower bounds, with the finite-n bound sharp when δ ≥ 1.
paraphrase · OpenMath supplies its own mathematical paraphrases and links; proof text is not republished.

Weibo Fu · Yanjun Han · Guanyang Wang · Jun Yan · Peng Zhang · Zhengqing Zhou · Preprint · Publication date Jul 27, 2026

Revision & attribution

Source revision: 2026-07-27. Observed Oct 13, 2026.

The authors report GPT-5.6 Pro assistance in proof discovery; the calibration theorem of Vlassis and Thomas and Grünbaum-type inequalities are mathematical inputs, not authors of this paper.