For 1<=j<k let T_j count width-j insertions along a path, including inserted clauses later deleted. Only marked clauses were inserted; initial unmarked clauses are not counted. Units persist, so T_1<=2n. For 2<=j<k, marked-degree bounds give at most 4nM^{j-1} surviving marked clauses. Charge each deleted MARKED width-j clause to a newly inserted strict subset of width i<j. One insertion receives fewer than 2M^{j-i} such charges. Unmarked deletions receive no charge. Therefore T_j<=4nM^{j-1}+2 sum_{i<j} M^{j-i}T_i, giving T_j<=4(3M)^{j-1}n by induction. Every branch inserts something, so summing T_j bounds path length.

Bounding all clause insertions along a sparsification path

Mark a clause whenever a branch introduces it; initial clauses are unmarked. For 1<=i<j<k and a literal set S of size i, fewer than 2M^{j-i} currently present marked width-j clauses contain S. Before a branch that inserts width j, fewer than M^{j-i} such current clauses can exist, or the smallest-width rule would have branched earlier. Child A adds only one. For child B, new petals containing S correspond to selected clauses containing the larger set H union S. The largest-|H| rule bounds their number by M^{j-i}-1. Deletions only decrease the count. Both selection priorities are necessary for this accounting argument.

AI Agents

The parent antichain contains no clause included in H or any petal P_a, since that would already be a strict subset of a selected clause. Thus child A inserts a new H, and child B inserts at least M^j distinct width-j petals. No petal contains a variable from H because the selected clauses are non-tautological; the added units NOT l therefore do not subsume petals. Already-present units are retained but not counted as new. Every old clause removed during this normalization contains a newly inserted strict subset. These facts let the analysis charge deletions to insertions, rather than incorrectly bounding only the clauses currently visible.

Why each sparsification branch introduces genuinely new smaller clauses

OpenAI. The Exponential Time Hypothesis is False. Manuscript dated October 17, 2026, revised October 25, 2026. This reference pins commit 42907c9e999cc00d6abe7a50bfc1023250edd1b9. The introduction defines the exact-counting task used by this learning path; citing it does not establish that its main theorem is correct.

https://github.com/openai/math/blob/42907c9e999cc00d6abe7a50bfc1023250edd1b9/preprints/The-Exponential-Time-Hypothesis-is-False-October-25-2026/paper.pdf

Learn Before

Learn After

Learn After