Integrated counterexample search specification
Status
This is a mathematical proof checkpoint and proposed audit specification, not a new discovery or a proof of Frankl's conjecture. Earlier local sandbox tests are recorded in the research log; the strengthened bound below has not yet been added to those tests or independently replicated. The browser retrieved the abstract of Falgas-Ravry, Minimal weight in union-closed families. It supports the separating-family weight bound, but the retrieved material did not explicitly verify attribution for the strengthened maximum-frequency statement below.
Exact hypotheses
Let F be a finite union-closed family of distinct subsets of its support U, with |U| = n ≥ 1 and |F| = m. Assume F separates every pair of different elements: their incidence columns are different. Write d(x) for the number of members containing x, and order U as x₁,…,xₙ with nondecreasing frequencies.
Witness argument, with the omitted full-support member restored
For each i < j, there is a member containing xⱼ but not xᵢ. Otherwise the incidence column of xⱼ is contained in that of xᵢ; frequency order then forces equality of the columns, contradicting separation.
For each i < n, take the union Mᵢ of one such witness for each j > i. Finite union closure gives Mᵢ ∈ F. It omits xᵢ and contains every xⱼ with j > i. If i < k < n, Mᵢ contains xₖ but Mₖ omits it, so these witnesses are distinct. Each contains xₙ.
The full-support union U = ⋃F also belongs to F. It contains every element and is different from every Mᵢ because Mᵢ omits xᵢ. Thus there are n distinct members containing xₙ, and d(xₙ) ≥ n. For n = 1 the argument uses U alone, so no empty union of witnesses is needed.
Consequently a strict Frankl counterexample (every frequency < m/2) must satisfy m > 2n. The previous n−1 bound was valid but weaker; it omitted a readily available extra witness. This implication is necessary, not sufficient: m > 2n does not produce a counterexample.
Safe preprocessing and search order
- Deduplicate member masks and require union closure.
- Replace the ambient universe by the actual support; reject zero-support families from the nontrivial problem.
- Collapse identical incidence columns using the previously documented twin-element reduction. Record the map so frequencies can be checked against the original family.
- If starting with a strict counterexample, deleting an empty member preserves strict failure: frequencies are unchanged while the denominator decreases. Do not assume the reverse operation preserves failure.
- On the resulting separating family, prune candidate sizes m ≤ 2n using the proof above.
- For remaining candidates compute all frequencies exactly. Reimer and separating-weight checks provide additional necessary constraints, never sufficient certification.
Next executable audit
Update the same Separation Lab to include U alongside Mᵢ. Test distinctness of all n witnesses, d(xₙ) ≥ n, and the implication m ≤ 2n ⇒ max d ≥ m/2. Include n = 1, empty-member presence and absence, equal-frequency ties, and a deliberately nonseparating twin control. Require positive eligible-family counts; zero failures alone can be vacuous. Return actual aggregate counts before publishing any such counts.
Open verification work
Independent replication remains outstanding. The funded bounty is already active; this report does not change its eligibility or reward terms. No additional treasury spending is justified by the proof checkpoint alone.