The encoding
Do the clauses forbid exactly the sign prefixes whose integer sums cross C? The census compares the Boolean and arithmetic routes assignment by assignment.
One object for existence. One certificate for impossibility.
The Boundary Written in Signs
A 1160-sign sequence stays within discrepancy 2 along every homogeneous arithmetic progression. At 1161, a machine-checked SAT certificate says every possible sequence fails. Inspect the witness, recompute its sums, and see what Tao's larger theorem did not replace.
1160
There exists a sign sequence this long with every checked sum inside -2 to +2.
1161
No sequence this long stays inside the same bound. The large certificate for that universal claim is cited here, not replayed here.
The witness bench
The paper printed these 1160 signs. Pick a step size d. The tape reads positions d, 2d, 3d and onward, always from zero.
Ready to scan the paper witness
This selects the homogeneous progression d, 2d, 3d. There is no translated starting point.
Scrub the running sum. Every earlier prefix counts too, not only the final sum.
x1 = -1. An edit stops being the published witness.
Running sum S(d,j), j from 0 to k
S(7,20) = 0
Actual indices and signs
Maximum |S(d,k)| for each d, click to inspect
d = 1d = 386, last nontrivial row for C = 2d = 1160
The green result proves an existential statement. One sequence works. It cannot prove the next sentence, because failing to append one more sign to this sequence says nothing about all the other sequences of length 1161.
The certificate bench
Here the universal claim is small enough to finish in your browser. The default case asks whether any 12-sign sequence can keep discrepancy at most 1.
Free encoding choice: for each progression prefix, the page emits one Boolean clause for every local sign pattern that would cross C. This is not the paper's more compact sequential-counter encoding.
Ready for C = 1, N = 12
Press the button. Direct sums and the generated CNF will inspect the same 4,096 assignments by separate routes.
Prefix inequalities35
Generated clauses5,734
Assignments tested4,096
Direct survivors0
CNF survivors0
Route disagreements0
The 8,191-step RUP refutation
The full-tree certificate first blocks all 4,096 complete assignments. Each leaf is accepted because its assumed signs falsify an original discrepancy clause. Then sibling clauses resolve upward until the last accepted clause is empty.
Loading clause 1
Preparing the proof check.
The certificate
Does each added clause follow by reverse unit propagation? The inspector checks every leaf against an input clause and every parent against its two accepted children.
The checker
Does the checker itself implement the rule correctly? The offline verifier uses separate code. This page's small checker is specialized to its full binary proof, not a general DRAT checker.
Which question?
Exactly where C = 2 fails
∃ x[1..1160] : all |S(d,k)| ≤ 2
∀ x[1..1161] : some |S(d,k)| > 2
∀ x[1..1161] : some |S(d,k)| > 2
Konev and Lisitsa's finite computation gives the exact cutoff. The witness bench runs the first line. Their large unsatisfiability certificate supports the second.
The check
Existence, recomputed here
PASS signs parsed: 1,160, each exactly +1 or -1
PASS sums enumerated: 8,374
PASS maximum absolute sum: 2
coordinates at the maximum: 894
first maximum: d = 1, k = 12, S = 2
SHA-256 of the 1160-character +- transcription: ffb5f644a7b702f25ef119078f3bcf1ad90e3ab541e06f03f61116e14a2c3106
Nonexistence, split honestly
PASS C = 1, N = 12: 35 inequalities, 5,734 clauses, 4,096 assignments rejected by both routes
CHECKING miniature full-tree RUP
1161 UNSAT: cited certificate not replayed in this session.
The artifact page linked below points to the public N = 1161 CNF, DRAT, and trimmed DRAT files. They are not loaded by this page. No local result is presented as their replay.
Published constants, not derived by this page
| Printed value | What the source says | Status here |
|---|---|---|
| 1160 / 1161 | The exact C = 2 boundary in Konev and Lisitsa. | The 1160 side is recomputed. The 1161 side is cited. |
| 12 | Every 12-term sign sequence has discrepancy at least 2. | Reproved here by all 4,096 assignments and RUP. |
| about 13 GB | Original 2014 DRUP certificate size. | Published rounded size only. |
| about 1.67 GB | Later DRUP certificate from the smaller encoding. | Published rounded size only. |
| 850.2 MB | Deletion-stripped RUP certificate reported in the journal paper. | Published one-decimal size only. |
| about five and a half hours | Reported drup-trim time for that RUP file on the authors' hardware. | Published rounded time only, not a benchmark for this device. |
Every uncertainty and free choice
Transcription. The signs were transcribed from Appendix B of the journal preprint. The SHA-256 value is our digest of that transcription, not a digest published by the authors. The independent verifier contains a second transcription and compares it byte for byte.
Large proof. We verified that the live artifact page separately links the N = 1161 CNF, DRAT proof, and trimmed DRAT proof. We did not download, hash, bundle, or replay the multi-gigabyte proof. Its byte identity and checker run remain unverified here.
Small encoding. Exact-pattern blocking clauses are our free choice because they are legible at N = 12. The paper used other, smaller encodings. The 8,191-step full binary RUP tree is also our deliberately verbose certificate, not theirs.
Conventions. A global exchange of + and - changes every sum's sign but not its absolute value. We use indices d, 2d through kd. These are homogeneous arithmetic progressions, not arbitrary translated progressions.
Trivial settings. At C = 2, k = 0 is zero by definition. Any k below 3, or any d greater than floor(N/3), has too few signs to cross 2. Those rows are drawn but are not evidence. Checking only d = 1, checking only terminal sums, or trying only two extensions of this witness would also be insufficient.
Edits. Flip a sign and the check remains exact, but the edited tape is yours. Reset before calling it the published witness.