we-solve (beta)

Math-2614 · mathematics · Combinatorics

Integral and fractional expectation thresholds within a constant factor

Status OpenLLM status Open unverified

Statement

Definitions and mathematical statement

Statement recorded in the supplied source.
Does one absolute constant C satisfy $q_f(F)<=C$ q(F) for every nonempty proper increasing family F on an arbitrary finite ground set, where integral and fractional covers both use cost budget one half?

Short English statement

Does one absolute constant C satisfy $q_f(F)<=C$ q(F) for every nonempty proper increasing family F on an arbitrary finite ground set, where integral and fractional covers both use cost budget one half?

Sources

Statement licence: CC-BY-4.0 · Source file

Contributions 1

Math-2614-A1 · Literature report · LLM-generated · unknown ·

OpenAI claim summary for Math-2614

The theorem covers every nonempty proper increasing family on a finite ground set with both cover budgets equal to one half. Its explicit universal factor $25\cdot512^4$ answers the entire constant-factor question. The empty-ground-set case has no such family.

Integral and fractional expectation thresholds within a constant factor

OpenAI's claim

Integral versus fractional thresholds: The claimed comparison bounds the fractional expectation threshold by a universal multiple of its integral version. Both versions are defined with the same containment-cover budget.

Mathematical statement of the claimed result

Mathematical claim 1.
For nonempty proper increasing $\mathcal F\subset2^X$, with finite nonempty $X$, let $q(\mathcal F)$ be the greatest $p\in[0,1]$ admitting a cover $\mathcal G$ such that every $H\in\mathcal F$ contains some $S\in\mathcal G$ and $\sum_{S\in\mathcal G}p^{|S|}\le1/2$. Define $q_f$ by allowing weights $g:2^X\to[0,1]$, requiring $\sum_{S\subseteq H}g(S)\ge1$ for each $H\in\mathcal F$ and $\sum_Sg(S)p^{|S|}\le1/2$. The exact claim is \[q(\mathcal F)\le q_f(\mathcal F)\le25\cdot512^4q(\mathcal F).\] The same budget $1/2$ is used on both sides, and the factor is independent of the ground-set size and minimal-member sizes.

Outline of the argument

Integral versus fractional thresholds: A multiscale random selector finds one member of the family that captures enough mass at every scale at once. Normalizing fractional cover weights on vertices gives a bounded average color for that member. Independent exponential color variables then force incompatible upper and lower expectations when the integral threshold is too small relative to the fractional threshold.

Formal verification

Family 175 describes Lean coverage for the integral/fractional threshold comparison and the discrete-convexity statement; graph decomposition is a later separate consequence.

Integral versus fractional thresholds: The manuscript links TalagrandDiscreteConvexity.lean (declaration OAI.TalagrandDiscreteConvexity.talagrand_discrete_convexity), TalagrandExpectationThreshold.lean (declaration OAI.TalagrandThreshold.talagrand_expectation_threshold_equivalence).

The documented selection includes this manuscript’s main assertion; that assertion retains the restrictions stated above.

This site has not run the Lean development. These links describe OpenAI’s selected formal statements and should be read with their stated scope.

Status caveat

OpenAI reports that an internal model produced the manuscripts. Their arguments have not been independently verified as proofs by this site. Any portion outside the documented formal scope may contain mistakes, and the catalogue label reports the announced mathematical claim.

Sources

Go to contribution →