Math and TheoryCritical hard-core influence bounds via nonbacktracking collisions
Problem and result
- Problem
- Spectral independence of the hard-core model at the uniqueness threshold λ_c(Δ)
- Posed in
- Bencs, Goldberg, Jenssen, Jerrum, Pete, Regts and Yin, arXiv:2608.09729, Section 5 (critical two-spin question)
- Status
- Partially resolved
- Result
- For every Δ ≥ 3, every n-vertex graph of maximum degree at most Δ, every activity 0 < λ ≤ λ_c(Δ) and every feasible pinning, each absolute row sum of the hard-core influence matrix is O_Δ(√n log n), with an explicit constant.
Abstract
For each fixed Δ ≥ 3, every row of the hard-core influence matrix has absolute sum O_Δ(√n log n) on every n-vertex graph of maximum degree at most Δ, at every activity up to the uniqueness threshold λ_c(Δ) and under every feasible pinning, with an explicit constant. The proof combines exact vertex-deletion identities, a known local squared-message contraction, a self-avoiding-walk transfer in the style of Sinclair, Srivastava, Štefankovič and Yin, and a finite form of the nonbacktracking collision argument of Bencs et al. It recovers, up to a logarithm, an O(√n) bound that was stated in 2025 and withdrawn in 2026. The constant is large, and the mixing-time consequence for Glauber dynamics is conditional on a published proposition.
Details
- Year
- 2026
- Discipline
- Theoretical computer science
- Area
- Sampling algorithms and spectral independence
- Subject
- Sampling algorithms and information theory
- Result type
- Theorem and reproducible proof package
- Formal proof
- Standalone Lean package
- Family
critical-hardcore- Keywords
- hard-core model, spectral independence, uniqueness threshold, Glauber dynamics, independent sets, nonbacktracking walks
Statement and scope
Formal scope. The influence bound for the actual hard-core Gibbs measure on every finite simple graph of maximum degree at most Δ, all activities up to λ_c(Δ) and all feasible pinnings is formalized in 32 Lean modules, including the regular completion and the nonbacktracking collision estimate. The Glauber-dynamics mixing corollary and the numerical observations on the constant are not formalized.
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.pdf368 KB- PDF on GitHub
papers/theoretical-computer-science/ critical-hardcore/ manuscript.pdf - LaTeX source
papers/theoretical-computer-science/ critical-hardcore/ manuscript.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/ critical-hardcore/ - Lean project
papers/33 Lean filestheoretical-computer-science/ critical-hardcore/ lean/ - Lakefile
papers/theoretical-computer-science/ critical-hardcore/ lean/ lakefile.lean - Toolchain
leanprover/lean4:v4.19.0 - Library roots
Reproduce
The commands below are quoted from papers/, which gives their context and working directory.
lake exe cache get
python3 verify.py- README
papers/theoretical-computer-science/ critical-hardcore/ README.md - Verification guide
papers/theoretical-computer-science/ critical-hardcore/ verification/ README.md - Verification record
papers/theoretical-computer-science/ critical-hardcore/ VERIFICATION.md - Authorship
papers/theoretical-computer-science/ critical-hardcore/ AUTHORSHIP.md - Repository guide
verification/README.md - Unfinished proofs
UNFINISHED.md
Source and prior work
Questions and answers
Does the hard-core model have Õ(√n) spectral independence at the uniqueness threshold?
This preprint proves that for each fixed Δ ≥ 3, every row of the hard-core influence matrix has absolute sum at most 1 + 12Δ(Δ−1)[λ/(1+λ)] r⌈log_{Δ−1} r⌉ with r = ⌊√(2Δn)⌋ + 1, on every n-vertex graph of maximum degree at most Δ, for all 0 < λ ≤ λ_c(Δ) and every feasible pinning. This addresses the hard-core case of the critical two-spin question of Bencs et al.; the general two-spin question and an O(√n) bound without the logarithm remain open. The constant is large: the bound beats the trivial bound n only for n ≥ 3.4·10⁶ when Δ = 3.
Wasn't an O(√n) critical bound already claimed?
Yes. Chen and Jiang stated an O(√n) critical hard-core influence bound in their APPROX/RANDOM 2025 paper and withdrew that claim in their 7 January 2026 arXiv revision. This preprint avoids the truncated-tree comparison of the withdrawn route and recovers that bound up to a logarithm; its ingredients, including the nonbacktracking collision argument of Bencs et al. and the self-avoiding-walk method of Sinclair, Srivastava, Štefankovič and Yin, are credited prior work.
Is the proof formally verified?
The influence bound for the actual hard-core Gibbs measure, all activities up to λ_c(Δ) and all feasible pinnings is formalized in 32 Lean 4 modules. The Glauber-dynamics mixing-time consequence is not formalized and is conditional on a published proposition of Chen and Jiang.
Cite
Citation file papers/. For the whole collection, use CITATION.cff or CITATION.bib.
@misc{goyal2026criticalhardcore,
author = {Goyal, Dev D.},
title = {Critical Hard-Core Influence Bounds via Nonbacktracking Collisions},
year = {2026},
month = oct,
note = {Preprint. Fully autonomous agentic research; publication responsibility: Dev D. Goyal},
url = {https://github.com/dvgyl/math-and-theory/tree/main/papers/theoretical-computer-science/critical-hardcore}
}