Theorem A -- proof

Sparsify a k-CNF into at most 2 ^ (ε N) pieces in which every variable occurs in at most c clauses, so that every variable has at most c (k - 1) neighbours. Each piece has only solutions of the original, so it contains no subcube of dimension D either, and the bounded-degree form of Theorem A bounds its solutions.

theorem Complexity.ClauseSet.SubcubeFree.card_solutions_le (k : ℕ) (hk : 1 ≤ k) {ε : ℝ} (hε : 0 < ε) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (N : ℕ) (φ : ClauseSet N) (D : ℕ), (∀ C ∈ φ, C.card ≤ k) → ¬ContainsSubcube (↑φ.solutions) D → ↑φ.solutions.card ≤ 2 ^ ((1 - 1 / ↑k + ε) * ↑N + C * ↑D)

Theorem A, internal form.