Counting sparsification -- the step is polynomial-time

The list-level counting-sparsification step (Cslib.Logic.PL.CNF.Sparsification.countingNext), tautology removal (Cslib.Logic.PL.CNF.Sparsification.removeTautologies), nontautological normalization (Cslib.Logic.PL.CNF.Sparsification.countingNormalize), and comparison with the counting thresholds countingThreshold M j = M ^ j (Cslib.Logic.PL.CNF.Sparsification.computableInPolyTime_countingThreshold_le) are polynomial-time on the framed encoding of formulas, for any encoding of the variables [OpenAI2026ETH, Appendix A.1].

Main results

• Cslib.Logic.PL.CNF.Sparsification.computableInPolyTime_countingThreshold_le: comparisons with countingThreshold M.
• Cslib.Logic.PL.CNF.Sparsification.computableInPolyTime_removeTautologies, Cslib.Logic.PL.CNF.Sparsification.computableInPolyTime_countingNormalize: tautology removal and nontautological normalization.
• Cslib.Logic.PL.CNF.Sparsification.computableInPolyTime_countingNextWith, Cslib.Logic.PL.CNF.Sparsification.computableInPolyTime_countingNext: the list-level counting step, for thresholds read from a runtime parameter and for fixed thresholds.
• Cslib.Logic.PL.CNF.Sparsification.computableInPolyTime_countingThreshold_le_binary, Cslib.Logic.PL.CNF.Sparsification.computableInPolyTime_isSparse_countingThreshold, Cslib.Logic.PL.CNF.Sparsification.computableInPolyTime_countingNext_countingThreshold: the thresholds countingThreshold M, the test for sparseness and the step for a base M given in binary at runtime.

References

• OpenAI, The Exponential Time Hypothesis is False, Appendix A.1

theorem Cslib.Logic.PL.CNF.Sparsification.computableInPolyTime_countingThreshold_le (M : ℕ) : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × ℕ) => decide (countingThreshold M p.1 ≤ p.2)) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) Turing.MultiTapeTM.encBool

Comparing the counting thresholds countingThreshold M j = M ^ j with a number is polynomial-time in unary.

theorem Cslib.Logic.PL.CNF.Sparsification.computableInPolyTime_isTautology {V : Type} [DecidableEq V] (encV : V ↪ List Bool) : Turing.MultiTapeTM.ComputableInPolyTime Clause.isTautology (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair encV Turing.MultiTapeTM.encBool)) Turing.MultiTapeTM.encBool

Tautology testing on a clause is polynomial-time.

theorem Cslib.Logic.PL.CNF.Sparsification.computableInPolyTime_removeTautologies {V : Type} [DecidableEq V] (encV : V ↪ List Bool) : Turing.MultiTapeTM.ComputableInPolyTime removeTautologies (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair encV Turing.MultiTapeTM.encBool))) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair encV Turing.MultiTapeTM.encBool)))

Removing tautological clauses from a formula is polynomial-time.

theorem Cslib.Logic.PL.CNF.Sparsification.computableInPolyTime_countingNormalize {V : Type} [DecidableEq V] (encV : V ↪ List Bool) : Turing.MultiTapeTM.ComputableInPolyTime countingNormalize (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair encV Turing.MultiTapeTM.encBool))) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair encV Turing.MultiTapeTM.encBool)))

Nontautological normalization (countingNormalize) is polynomial-time.

theorem Cslib.Logic.PL.CNF.Sparsification.computableInPolyTime_countingNextWith {V : Type} [DecidableEq V] (encV : V ↪ List Bool) {P : Type} {encP : P ↪ List Bool} {θ : P → ℕ → ℕ} (hθ : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : P × ℕ × ℕ) => decide (θ x.1 x.2.1 ≤ x.2.2)) (Turing.MultiTapeTM.encPair encP (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary)) Turing.MultiTapeTM.encBool) (k : ℕ) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : P × CNF V × Bool) => countingNext (θ x.1) k x.2.1 x.2.2) (Turing.MultiTapeTM.encPair encP (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair encV Turing.MultiTapeTM.encBool))) Turing.MultiTapeTM.encBool)) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair encV Turing.MultiTapeTM.encBool)))

The counting step for runtime thresholds θ p is polynomial-time, charging the encoding of the parameter p.

theorem Cslib.Logic.PL.CNF.Sparsification.computableInPolyTime_countingNext {V : Type} [DecidableEq V] (encV : V ↪ List Bool) {θ : ℕ → ℕ} (hθ : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × ℕ) => decide (θ p.1 ≤ p.2)) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) Turing.MultiTapeTM.encBool) (k : ℕ) : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : CNF V × Bool) => countingNext θ k p.1 p.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair encV Turing.MultiTapeTM.encBool))) Turing.MultiTapeTM.encBool) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair encV Turing.MultiTapeTM.encBool)))

The list-level counting-sparsification step is polynomial-time.

The counting thresholds for a runtime base

theorem Cslib.Logic.PL.CNF.Sparsification.computableInPolyTime_countingThreshold_le_binary : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : ℕ × ℕ × ℕ) => decide (countingThreshold x.1 x.2.1 ≤ x.2.2)) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary)) Turing.MultiTapeTM.encBool

Comparing the counting thresholds countingThreshold M j = M ^ j with a number is polynomial-time for a runtime base M in binary, with j and the compared number in unary.

theorem Cslib.Logic.PL.CNF.Sparsification.computableInPolyTime_isSparse_countingThreshold {V : Type} [DecidableEq V] (encV : V ↪ List Bool) (k : ℕ) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : ℕ × CNF V) => isSparse (countingThreshold x.1) k x.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair encV Turing.MultiTapeTM.encBool)))) Turing.MultiTapeTM.encBool

Sparseness for a runtime base. The test for sparseness against the thresholds countingThreshold M, for a base M given in binary at runtime, is polynomial-time.

theorem Cslib.Logic.PL.CNF.Sparsification.computableInPolyTime_countingNext_countingThreshold {V : Type} [DecidableEq V] (encV : V ↪ List Bool) (k : ℕ) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : ℕ × CNF V × Bool) => countingNext (countingThreshold x.1) k x.2.1 x.2.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair encV Turing.MultiTapeTM.encBool))) Turing.MultiTapeTM.encBool)) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair encV Turing.MultiTapeTM.encBool)))

The counting step for a runtime base. The counting-sparsification step for the thresholds countingThreshold M, for a base M given in binary at runtime, is polynomial-time.