structure MoserCorrectness.Literal (n : ℕ) : Type

A propositional literal over $n$ variables: a variable index in $\text{Fin}\ n$ together with a Boolean polarity (true = positive, false = negated).

• var : Fin n
• polarity : Bool

structure MoserCorrectness.Clause (n k : ℕ) : Type

A $k$-clause over $n$ variables: an indexed family of $k$ literals (interpreted as their disjunction).

• lits : Fin k → Literal n

@[reducible, inline]

abbrev MoserCorrectness.Assignment (n : ℕ) : Type

A Boolean assignment to $n$ variables.

def MoserCorrectness.Clause.satisfied {n k : ℕ} (C : Clause n k) (σ : Assignment n) : Prop

The clause $C$ is satisfied by the assignment $\sigma$ if at least one of its literals evaluates to true.

structure MoserCorrectness.KCNF (n m k : ℕ) : Type

A $k$-CNF formula over $n$ variables consisting of $m$ clauses, each of width exactly $k$.

• clauses : Fin m → Clause n k

def MoserCorrectness.KCNF.satisfiable {n m k : ℕ} (φ : KCNF n m k) : Prop

A $k$-CNF formula is satisfiable if some assignment satisfies every one of its clauses.

def MoserCorrectness.Clause.sharesVarWith {n k : ℕ} (C D : Clause n k) : Prop

Two clauses share a variable if some literal of $C$ and some literal of $D$ refer to the same variable index.

def MoserCorrectness.KCNF.boundedDegree {n m k : ℕ} (φ : KCNF n m k) (d : ℕ) : Prop

A $k$-CNF formula has bounded degree $d$ if every clause shares a variable with at most $d$ other clauses.

theorem MoserCorrectness.entropy_compression_arith (n k : ℕ) (hk : k ≥ 3) : n + (n + 2) * (k - 1) + 1 < k * (n + 2)

Arithmetic inequality used in the entropy-compression argument: for $k \ge 3$, $n + (n+2)(k-1) + 1 < k(n+2)$.

theorem MoserCorrectness.entropy_compression_pow_bound (n k : ℕ) (hk : k ≥ 3) : 2 ^ n * 2 ^ ((n + 2) * (k - 1) + 1) < 2 ^ (k * (n + 2))

Exponentiating entropy_compression_arith: $2^n \cdot 2^{(n+2)(k-1)+1} < 2^{k(n+2)}$ for $k \ge 3$.

noncomputable def MoserCorrectness.resampleFn {n k : ℕ} (vars : Fin k → Fin n) (σ : Fin n → Bool) (b : Fin k → Bool) : Fin n → Bool

Resample function used by Moser's algorithm: given a list vars of variable indices and fresh random bits b, replace the values of $\sigma$ on the listed variables by the corresponding bits and leave the others unchanged.

noncomputable def MoserCorrectness.stepSt {n k : ℕ} (vars_seq : ℕ → Fin k → Fin n) (σ₀ : Fin n → Bool) (bits : ℕ → Fin k → Bool) : ℕ → Fin n → Bool

The state of the resampling process after $t$ steps, starting from $\sigma_0$, where step $t$ resamples the variables vars_seq t using the random bits bits t.

theorem MoserCorrectness.recover_prev_state {n k : ℕ} (vars_seq : ℕ → Fin k → Fin n) (σ₀ : Fin n → Bool) (bits₁ bits₂ violating : ℕ → Fin k → Bool) (hviol₁ : ∀ (t : ℕ) (i : Fin k), stepSt vars_seq σ₀ bits₁ t (vars_seq t i) = violating t i) (hviol₂ : ∀ (t : ℕ) (i : Fin k), stepSt vars_seq σ₀ bits₂ t (vars_seq t i) = violating t i) (t : ℕ) (heq_next : stepSt vars_seq σ₀ bits₁ (t + 1) = stepSt vars_seq σ₀ bits₂ (t + 1)) : stepSt vars_seq σ₀ bits₁ t = stepSt vars_seq σ₀ bits₂ t

Reversibility of the Moser resampling step: if two runs of the algorithm agree on the post-state after step $t$ and on the violating clause values at every step, then they must already agree on the state at time $t$. This underlies the entropy-compression argument.

structure MoserCorrectness.EntropyCompression (n m k ℓ : ℕ) (φ : KCNF n m k) : Type

Bundle produced by the entropy-compression argument: a set of "failing" random strings of size at most $2^n \cdot 2^{\ell(k-1)+1}$, together with a proof that any string outside this set witnesses satisfiability of $\varphi$.

• failingStrings : Finset (Fin (2 ^ (k * ℓ)))
• card_bound : self.failingStrings.card ≤ 2 ^ n * 2 ^ (ℓ * (k - 1) + 1)
• success_implies_sat (x : Fin (2 ^ (k * ℓ))) : x ∉ self.failingStrings → φ.satisfiable

noncomputable def MoserCorrectness.entropy_compression_exists {n m k : ℕ} (hk : k ≥ 3) (φ : KCNF n m k) (hd : φ.boundedDegree (2 ^ (k - 3))) (ℓ : ℕ) (hℓ : ℓ ≥ 1) : EntropyCompression n m k ℓ φ

Existence of the entropy-compression bundle (Lemmas 6.6.7–6.6.8): for any $k$-CNF formula with $k \ge 3$ and bounded degree $2^{k-3}$, and any $\ell \ge 1$, the set of $\ell$-step random-bit strings for which Moser's algorithm fails has cardinality at most $2^n \cdot 2^{\ell(k-1)+1}$, and every successful string yields a satisfying assignment.

theorem MoserCorrectness.moser_correctness {n m k : ℕ} (hk : k ≥ 3) (φ : KCNF n m k) (hd : φ.boundedDegree (2 ^ (k - 3))) : φ.satisfiable

Moser's correctness theorem (Theorem 6.6.6): every $k$-CNF formula with $k \ge 3$ in which each clause shares a variable with at most $2^{k-3}$ other clauses is satisfiable. The proof uses an entropy-compression / pigeonhole argument on $\ell = n+2$ random-bit blocks.