Infinite $k$ -SAT: bounded variable occurrence implies a global satisfying assignment, at any cardinality

Proved

QLLL.SAT.exists_assignment_forall

by sattath · Oct 6, 2026 · Mathlib 0df444a (Lean v4.33.1)

k-satlovasz-local-lemmaquantum-lll

A clause is a disjunction of literals over boolean variables, and an assignment satisfies it if at least one literal evaluates to true. Let $\mathcal{V}$ be an arbitrary set of variables and let $(C_i)_{i \in I}$ be clauses over $\mathcal{V}$ indexed by an arbitrary set $I$ ; neither set needs to be finite or countable. Let $k \ge 1$ and $D \ge 1$ be integers such that:

every clause $C_i$ involves exactly $k$ distinct variables;
every variable occurs in at most $D$ clauses of every finite subfamily (equivalently, in at most $D$ clauses in total);
$D \cdot e \cdot k \le 2^{k}$ .

Then there is a single assignment $a : \mathcal{V} \to \{0,1\}$ satisfying every clause $C_i$ .

This extends Corollary 2 of Ambainis, Kempe and Sattath to infinite formulas. The conclusion is a single assignment because the space of all assignments is compact; the corresponding quantum statement for subspaces fails, since subspace lattices have no such compactness.

Preamble

import Definitions.Def_QLLL_LocalLemma_Basic
import Definitions.Def_QLLL_Classical_KSAT
import Definitions.Def_QLLL_Classical_InfiniteKSAT
import Mathlib
import Std.Sat.CNF

open QLLL
open QLLL.SAT
open Finset Std.Sat

Formal statement

theorem QLLL.SAT.exists_assignment_forall {V ι : Type*} [DecidableEq V]
    (C : ι → CNF.Clause V) (k D : ℕ) (hk : 1 ≤ k) (hD1 : 1 ≤ D)
    (hvars : ∀ i, (clauseVars' (C i)).card = k)
    (hdeg : ∀ (v : V) (T : Finset ι),
      (T.filter fun i => v ∈ clauseVars' (C i)).card ≤ D)
    (hDk : (D : ℝ) * (Real.exp 1 * k) ≤ 2 ^ k) :
    ∃ a : V → Bool, ∀ i, CNF.Clause.eval a (C i) = true := by sorry

Source

Not in the paper; an infinite extension of Corollary 2. Formalization companion to Ambainis, Kempe and Sattath, A Quantum Lovász Local Lemma, arXiv:0911.1696; see the blueprint https://sattath.github.io/Quantum-Lovasz-Local-Lemma/blueprint/

View graph

Infinite kkk-SAT: bounded variable occurrence implies a global satisfying assignment, at any cardinality

Infinite $k$ -SAT: bounded variable occurrence implies a global satisfying assignment, at any cardinality