Frankl’s Conjecture at 0.382345

Known Stuff#

The conjecture#

A finite family 𝓕 of subsets of a finite ground set U is union-closed when A ∪ B belongs to 𝓕 whenever A and B do. For a coordinate i, its abundance is the fraction of members containing it:

f_{i} (𝓕) = \frac{| {A \in 𝓕 : i \in A} |}{| 𝓕 |} .

Frankl’s conjecture asserts that every nontrivial finite union-closed family has an abundant coordinate:

\max_{i \in U} f_{i} (𝓕) \geq \frac{1}{2} .

The conjecture remains open. “Nontrivial” here means nonempty and not the singleton family containing only the empty set.

The entropy obstruction#

Let X be uniform on 𝓕. Then its Shannon entropy is log |𝓕|. If X and Y are coupled copies, union closure keeps X ∪ Y inside 𝓕, so maximality of the uniform law gives

H (X \cup Y) \leq \log | 𝓕 | = H (X) .

Gilmer’s method derives the opposite strict inequality when every coordinate mean is small. Alweiss, Huang, and Sellke sharpened this route to the explicit peer-reviewed constant (3−√5)/2 [1] [2]. Sawin introduced a mixture of independent and negatively dependent couplings; Yu reduced its optimization to finite marginal laws [3] [4].

The coupling frontier#

The local objective#

Write h for binary entropy, p ⊔ q for the success probability of an independent Boolean union, and d for Yu’s maximum-entropy dependent-union parameter:

\begin{aligned} h (p) & = - p \log p - (1 - p) \log (1 - p), \\ p ⊔ q & = p + q - p q, \\ d (p, q) & = \min {p + q, \max {p, q, \frac{1}{2}}} . \end{aligned}

Let π be a finite symmetric law of a pair (P,Q) with common marginal μ and mean at most t. Set

\begin{aligned} A (μ) & = \iint h (p ⊔ q) d μ (p) d μ (q), \\ B (μ) & = \int h (p) d μ (p), \\ C (π) & = \int h (d (p, q)) d π (p, q) . \end{aligned}

The finite coupling problem is to prove a positive affine gap uniformly over π. Its solution supplies the one-coordinate inequality that the chain rule can sum.

The evidence frontier#

The previously established explicit peer-reviewed constant was

\frac{3 - \sqrt{5}}{2} = 0.381966011250105 \dots .

Yu reported a numerical certificate at 0.38234. Cambie reduced the same scheme to two bivariate cases and reported the apparent ceiling 0.382345533366703…, but described the closing Maple and graphical verification as less rigorous [5]. Liu proved an analytic strict-improvement mechanism for conditionally IID couplings; the displayed value 0.382709087918741 remains conditional on an infinite matrix-positivity conjecture and an unproved global optimizer shape [6].

Two structural questions#

Bidual Horn functions#

A Boolean function is Horn exactly when its false points are intersection-closed. It is bidual Horn when its true points are also union-closed. Lozin and Zamaraev proved several Horn subclasses and left the bidual case open, identifying the self-dual subclass as a difficult core [8].

The binary semigroup seam#

Zargar lifted intersection-closed families to multiplication-closed semigroup fibers and proved weighted half-frequency theorems for a range of fiber sizes. His argument isolates the binary case k = 2, m = 1, corresponding to weights 2^−|A|, but its published concavity calculation degenerates at exactly that parameter [9].

New Stuff#

The rational abundance theorem#

Theorem. Let 𝓕 be a nonempty finite union-closed family of subsets of a finite set. If 𝓕 is not the singleton family containing only the empty set, then some coordinate belongs to strictly more than 76,469/200,000 of the members of 𝓕.

\max_{i \in U} f_{i} (𝓕) > \frac{76469}{200000} = 0.382345 > \frac{3 - \sqrt{5}}{2} .

The complete implication from the finite family to the rational scalar certificate is checked in Lean. The theorem declaration is Frankl.unionClosed_exists_abundant_coordinate.

The finite entropy bridge#

Conditional laws#

Enumerate the ground set and regard each member of 𝓕 as a Boolean vector. For a finite law X on the cube, reveal its coordinates in order. At coordinate j, the conditional success probability

P_{j} = \Pr (X_{j} = 1 | X_{< j})

is a finite random variable whose mean is the unconditional frequency of coordinate j. Null conditioning fibers are assigned probability zero and contribute no entropy.

Two symmetric self-couplings are constructed recursively. The first is independent. The second couples the revealed prefixes symmetrically and, conditional on a prefix pair with success probabilities p and q, uses a Boolean coupling whose union has parameter d(p,q). Both output coordinates have the original marginal law.

The global contradiction#

The scalar theorem proved below states that every finite symmetric orbit law of mean at most t = 76,469/200,000 satisfies

\frac{193}{200} A (μ) + \frac{7}{200} C (π) \geq (1 + 10^{- 7}) B (μ) .

Apply this at every coordinate. Shannon’s chain rule identifies the sum of the marginal terms with H(X). Conditioning cannot increase entropy, so the independent and dependent sums are lower bounds for the entropies of the two coupled unions. Hence

\frac{193}{200} H (X^{0} \cup Y^{0}) + \frac{7}{200} H (X^{1} \cup Y^{1}) \geq (1 + 10^{- 7}) H (X) .

If X is uniform on a union-closed 𝓕, both union laws remain supported on 𝓕, so the left side is at most log |𝓕|. When |𝓕| ≥ 2, the right side is strictly larger than log |𝓕|, a contradiction. A singleton family other than {∅} has a coordinate of frequency one.

The scalar proof#

Orbit reduction#

The proof begins with an arbitrary finite symmetric law π. If its mean is below t, adjoining an atom at (1,1) raises the mean to exactly t without increasing the normalized obstruction. On the exact-mean slice the affine gap is concave in π, so a one-moment extreme-point theorem reduces its minimum to at most two unoriented orbits.

A half-support inequality replaces every coordinate above one half by a mean-preserving mixture at one half and one. Exact spread contractions then leave three canonical possibilities: a single low diagonal orbit, two low diagonal orbits, or one low diagonal orbit paired with an endpoint orbit. The first two families are nonnegative by analytic Jensen-deficit estimates. The endpoint family carries the final parameters a and q.

Endpoint closure#

Half support forces the endpoint coordinate into the dichotomy q ≤ 1/2 or q = 1; the open strip between them is unrealizable. For 1/4 ≤ a ≤ t and 0 ≤ q ≤ 1/2, condition away the deterministic coordinate and set

r = \frac{a (1 - 2 t) + t q}{1 + q - a - t}, M = \max {a, q} .

Using the actual support ceiling M, rather than the global ceiling 1/2, bounds the independent-entropy loss by the marginal deficit with coefficient

Ψ (M, r) = \frac{193}{200} (1 - t) (\frac{M}{M + r - M r} + \frac{1 - \frac{4 r}{3}}{1 - r}) \leq 1 + 10^{- 7} .

Monotonicity in r reduces the last inequality to one quadratic sign on q ≤ a and one cubic sign on a ≤ q. The remaining saturated centered objective becomes, in the complement coordinate y = 1−r,

K (y) = \frac{193}{200} {(1 - t)}^{2} h (y^{2}) + \frac{7}{200} (2 (1 - t) y - y^{2}) \log 2 - (1 + 10^{- 7}) (1 - t) y h (y) .

On 1−t ≤ y ≤ 21/25, the sign changes of the third derivative are controlled by the increasing cubic

Q (y) = 10000001 y^{3} + 23841483 y^{2} - 30000003 y + 3841481 .

Thus K″ reaches its minimum at an endpoint. Rational atanh enclosures make both endpoint values positive, and a rational supporting line proves K positive throughout the interval.

The edge q = 1 needs no certificate. Replacing its deterministic endpoint atom by the symmetric orbit at q = a preserves the marginal law and the independent term and can only decrease the dependent term. In the endpoint objective J,

J (a, a) \leq J (a, 1) .

The reflected kernel#

Only the rectangle 0 ≤ a ≤ 1/4, 0 ≤ q ≤ 1/2 remains. A small expression language represents rational operations, binary entropy, capped entropy, and self-union. Its Lean theorem proves that a successful subdivision certificate implies nonnegativity throughout the represented rectangle.

The committed trace contains rational boxes and closed proof data. Every leaf uses certified interval values, first-order slope bounds, or an analytic entropy-zero corner rule; every internal node proves exact coverage. The generated files reduce by definitional equality to a successful checker result. Python is neither invoked nor trusted by Lean.

The bidual Horn theorem#

Theorem. Every bidual Horn Boolean function with at least two false points has a good coordinate. Consequently, Frankl’s conjecture holds for every bidual Horn function and, in particular, every self-dual Horn function.

The density dichotomy#

Karpas proved that a union-closed subfamily of the n-cube with at least 2ⁿ⁻¹ members has an abundant coordinate [7]. The source interchanges two directed-influence labels; the project audit reconstructs the theorem from raw edge counts, with the sign corrected.

Let F and T be the false and true points of a bidual Horn function. They partition the cube; F is intersection-closed and T is union-closed. Write F^* for set complementation inside the ground set. De Morgan’s law makes F^* union-closed.

The conclusion#

If |T| ≥ 2ⁿ⁻¹, Karpas supplies a coordinate i abundant in T. Since exactly half the cube contains i,

| F_{i} | = 2^{n - 1} - | T_{i} | \leq \frac{| F |}{2} .

If |T| < 2ⁿ⁻¹, then |F| > 2ⁿ⁻¹. Karpas applied to F^* gives |(F^*)_i| ≥ |F|/2, while |(F^*)_i| = |F|−|F_i|. Again i is rare among the false points, which is exactly a good Horn coordinate.

This proof closes the class question; it does not transform an arbitrary Horn function into a bidual one and does not strengthen the universal constant.

The binary semigroup theorem#

Theorem. For every probability measure μ on [0,1] of mean 0 < φ < 1/2, Zargar’s binary functional satisfies the sharp inequality F_2,1(μ) ≥ φ(1−2φ) log 2 > 0.

The functional#

Retain h for binary entropy, put η(u) = −u log u, and set L = log 2. Zargar’s specialized unary and binary kernels are

\begin{aligned} u_{2, 1} (x) & = h (x) + x L, \\ g_{2, 1} (x, y) & = η ((1 - x) (1 - y)) \\ + η (\frac{x + y}{2}) + η (\frac{x + y - 2 x y}{2}), \\ F_{2, 1} (μ) & = \iint g_{2, 1} (x, y) d μ (x) d μ (y) - \int u_{2, 1} (x) d μ (x) . \end{aligned}

For a signed measure ν of total mass and first moment zero, the quadratic form of the first summand of g vanishes. After integration by parts in the second summand and a convergent power expansion in the third, the rest is

Q (ν) = - \frac{1}{2} \int_{0}^{\infty} {(\int_{0}^{1} e^{- s x} N (x) d x)}^{2} d s - \sum_{j \geq 2}^{\infty} \frac{{(\int {(1 - 2 x)}^{j} d ν (x))}^{2}}{4 j (j - 1)} \leq 0,

where N(x) = ν([0,x]). Thus F_2,1 is concave on the compact convex set of probability measures of fixed mean φ.

The extremizers#

A concave functional reaches its minimum at an extreme one-moment law, hence at a law supported on at most two points. An interior two-point minimizer would have a first-variation potential f with matching endpoint derivatives and nonnegative endpoint second derivatives. But direct differentiation gives

\frac{d}{d t} [t f^{″} (t)] = - \frac{1 - 2 φ}{{(1 - t)}^{2}} - 𝔼 [\frac{Z}{{(Z + t)}^{2}}] - 𝔼 [\frac{Z {(1 - 2 Z)}^{2}}{{(Z + (1 - 2 Z) t)}^{2}}] < 0 .

Rolle’s theorem would force an interior zero of f″, after which the strict decrease of t f″ makes the upper endpoint negative, a contradiction.

Let β_φ = (1−φ)δ₀+φδ₁. A remaining extreme law supported at zero has the form (1−φ/x)δ₀+(φ/x)δ_x, with φ ≤ x ≤ 1, and direct simplification gives

F_{2, 1} (μ) - F_{2, 1} (β_{φ}) = \frac{φ}{x} [(1 - φ) h (x) - 2 φ (1 - x) L] \geq 0 .

The inequality follows because h(x)/(1−x) is increasing and h(φ) ≥ 2φ log 2 on [0,1/2]. For the family supported at one, put L_x = h((1−x)/2) and

\begin{aligned} A_{1} (x) & = h (x) - 2 x L_{x}, \\ C_{1} (x) & = 2 L_{x} - (2 - x) h (x) - 2 {(1 - x)}^{2} L . \end{aligned}

Multiplying the functional difference by the positive factor (1−x)²/(1−φ) gives A₁(x)+φC₁(x). Exact differentiation proves C₁ ≤ 0 and A₁+C₁/2 ≥ 0; since φ ≤ 1/2, the difference is nonnegative. Hence β_φ minimizes F_2,1, with value φ(1−2φ) log 2.

The weighted consequence#

Substituting the sharp binary inequality into Zargar’s semigroup lift closes the omitted case. Every finite intersection-closed family 𝓒 with at least two members has a coordinate i satisfying

\sum_{A \in 𝓒, i \notin A} 2^{- | A |} > \frac{1}{2} \sum_{A \in 𝓒} 2^{- | A |} .

Set complementation gives the dual statement: every nontrivial union-closed family 𝓖 has a coordinate i with

\sum_{A \in 𝓖, i \in A} 2^{| A |} > \frac{1}{2} \sum_{A \in 𝓖} 2^{| A |} .

Strictness follows from the equality case of the lifted entropy comparison: stationarity in the three-element coordinate semigroup would force every base coordinate to be constant, impossible for a family with at least two members. This is a theorem for nonuniform weights, not the uniform distribution in Frankl’s conjecture.

Bookkeeping#

Old and new#

Seam	Previous boundary	Present boundary	Evidence
Explicit universal abundance	(3−√5)/2	76,469/200,000	Lean
Entropy implication	Analytic scheme	Finite family-to-certificate bridge	Lean
Endpoint certificate	Low, high-residual, and `q` = 1 traces	Low rectangle only	Lean
Bidual Horn class	Stated open in 2024	Density dichotomy proves the conjecture	Independent written audit
Zargar `k` = 2, `m` = 1	Degenerate concavity seam	Sharp functional and weighted theorem	Independent written audit

Verification#

Lean boundary#

The publication theorem, the finite entropy bridge, the scalar orbit inequality, the support-aware endpoint proof, and the reflected low-rectangle trace compile under the repository’s strict Lean gate. The five publication-facing declarations have the reviewed transitive axiom set propext, Classical.choice, and Quot.sound.

The gate rejects warnings, automatic implicit variables, sorry, admit, project axioms, unsafe, partial, native_decide, external declarations, tactic escape hatches, and linter suppressions. Environment linters and a byte-exact axiom snapshot pass.

The Lean libraries are compartmentalized. lake build Frankl builds only this development; lake build MatrixMortality builds only the matrix-mortality development. The repository release gate intentionally builds both.

Independent oracle#

A separate Python program evaluates the reduced objectives with 160-bit Arb interval arithmetic. At 76,469/200,000 it reports 41,080 assessed rational boxes and 20,573 certified leaves across the endpoint and two diagonal families. The program reproduces the earlier 19,099/50,000 audit when given that historical target.

The oracle is a regression check and parameter-search instrument. No Lean declaration imports its output. Regenerating the committed low trace from the Lean generator is byte-for-byte reproducible.

Scope and priority#

The rational theorem improves the previous explicit peer-reviewed universal constant and is fully kernel-checked. It does not prove the conjectured half bound. It is numerically below Cambie’s 0.382345533366703… candidate and Liu’s conditional 0.382709087918741 candidate, and it does not claim to dominate Liu’s nonquantitative analytic strict-improvement theorem.

The priority search closed on 8 August 2026. No earlier source was located for an explicit rigorous constant above (3−√5)/2, for the bidual Horn density corollary, or for the binary k = 2, m = 1 theorem. These are bounded literature findings, not claims about unindexed manuscripts or private communication. None of the present results has passed external peer review.

The bidual Horn and binary semigroup theorems have complete independent written proofs but are not Lean-formalized. They are segregated from the kernel-checked universal bound throughout the source ledger.

Artifacts#

References#

Justin Gilmer, “A Constant Lower Bound for the Union-Closed Sets Conjecture,” 2022. arXiv:2211.09055.
Ryan Alweiss, Brice Huang, and Mark Sellke, “Improved Lower Bound for Frankl’s Union-Closed Sets Conjecture,” Electronic Journal of Combinatorics 31(3), 2024. doi:10.37236/12232.
Will Sawin, “An Improved Lower Bound for the Union-Closed Set Conjecture,” 2023. arXiv:2211.11504.
Lei Yu, “Dimension-Free Bounds for the Union-Closed Sets Conjecture,” Entropy 25(5), 767, 2023. doi:10.3390/e25050767.
Stijn Cambie, “Better Bounds for the Union-Closed Sets Conjecture Using the Entropy Approach,” revised 2025. arXiv:2212.12500.
Jingbo Liu, “Improving the Lower Bound for the Union-Closed Sets Conjecture via Conditionally IID Coupling,” CISS 2024. doi:10.1109/CISS59072.2024.10480167.
Ilan Karpas, “Two Results on Union-Closed Families,” 2017. arXiv:1708.01434v1.
Vadim Lozin and Viktor Zamaraev, “Union-Closed Sets and Horn Boolean Functions,” Journal of Combinatorial Theory, Series A 202, 105818, 2024. doi:10.1016/j.jcta.2023.105818.
Masoud Zargar, “The Union-Closed Sets Conjecture for Non-Uniform Distributions,” 2023. arXiv:2305.19338v2.