Unbounded coalesced-mass certificates for resolution trees

Dev D. Goyal

Unbounded coalesced-mass certificates for resolution trees

Dev D. Goyal · 2026 · Research preprint, not externally peer reviewed

Problem and result

Problem: Coalesced clause-mass certificate for resolution trees (Kunisky's Komlós approach)
Posed in: Attributed to Kunisky, arXiv:2111.02974v1, Conjecture 4.4 and Eq. (41); literal correspondence unverified
Status: Determined exactly
Result: For every n ≥ 3, the coalesced clause-mass certificate over finite unrestricted resolution refutations of the formula of all 2ⁿ full signed clauses has exact supremum n + 1; a three-variable witness exceeds 61/25 > 1 + √2.

Abstract

A coalesced dyadic clause-mass functional has exact supremum n+1 on the stated unrestricted resolution-tree class and is unbounded across dimensions.

Details

Year: 2026
Discipline: Theoretical computer science
Area: Proof complexity
Subject: Proof complexity
Result type: Standalone theorem and reproducible proof package
Formal proof: Standalone Lean package
Family: kunisky
Keywords: proof complexity, resolution, resolution trees, clause mass, Kunisky

Statement and scope

Formal scope. The internally defined resolution-tree functional and proof class are formalized. No unconditional identification with an external conjecture or a regular proof class is claimed.

A Lean check establishes only the formal statement that is checked. It does not establish novelty, historical priority or a faithful transcription of an external source. Known gaps are listed in UNFINISHED.md; the authorship disclosure describes how the results were produced.

Manuscript

PDF on this site: manuscript.pdf 277 KB
PDF on GitHub: papers/theoretical-computer-science/kunisky/paper.pdf
LaTeX source: papers/theoretical-computer-science/kunisky/paper.tex

Formal proof

This result has a standalone Lean 4 package, separate from the shared library. Build it with the toolchain and instructions given in its README.

Proof package

papers/theoretical-computer-science/kunisky/

Lean project

papers/theoretical-computer-science/kunisky/formalization/ 17 Lean files

Lakefile

papers/theoretical-computer-science/kunisky/formalization/lakefile.lean

Toolchain

leanprover/lean4:v4.19.0

Library roots

Reproduce

The commands below are quoted from papers/theoretical-computer-science/kunisky/README.md, which gives their context and working directory.

Contents and build

latexmk -pdf -interaction=nonstopmode -halt-on-error -outdir=.build paper.tex
cp .build/paper.pdf paper.pdf
python3 checks/verify_exact.py
cd formalization
lake exe cache get
bash build.sh
PYTHONDONTWRITEBYTECODE=1 python3 -m unittest discover -s tests -v

README: papers/theoretical-computer-science/kunisky/README.md
Formalization notes: papers/theoretical-computer-science/kunisky/FORMALIZATION.md
Source provenance: papers/theoretical-computer-science/kunisky/SOURCE_PROVENANCE.md
Authorship: papers/theoretical-computer-science/kunisky/AUTHORSHIP.md
Repository guide: verification/README.md
Unfinished proofs: UNFINISHED.md

Source and prior work

Questions and answers

What does this paper prove about the resolution certificate attributed to Kunisky?

For the explicitly defined functional, which coalesces dyadic leaf masses by clause label before square roots, the supremum over unrestricted (including nonregular) resolution refutations of the full n-variable formula is exactly n + 1 for n ≥ 3. If Kunisky's Conjecture 4.4 uses exactly this functional and proof class, this contradicts a universal bound 1 + √2; that correspondence is unverified.

Does it give a lower bound for the Komlós constant?

No. It gives no discrepancy bound and does not exclude choosing a suitable proof for each formula: the same formula has a balanced read-once refutation whose certificate is only (n+1)/2^(n/2).

Is the proof formally verified?

Lean 4 formalizes the internally defined functional and proof class, the exact supremum n + 1 and unboundedness. It does not authenticate the external conjecture.

Cite

Citation file papers/theoretical-computer-science/kunisky/CITATION.bib. For the whole collection, use CITATION.cff or CITATION.bib.

@unpublished{Goyal2026CoalescedMass,
  author = {Dev D. Goyal},
  title = {Unbounded coalesced-mass certificates for resolution trees},
  year = {2026},
  note = {Research note. No first-priority claim is made}
}