The certificate
Correction to the supplied spec
The paper says its 716-tournament set came from an order-dependent deletion process; it does not define that subset from the tournament axioms alone. This page therefore regenerates and sweeps the full 2,086-tournament domain instead. The larger sweep proves the same bounded null without copying the unlicensed upstream graph list.
- The claim
- No neutral resolute binary-gamma winner rule exists on the stated finite domain.
- Domain swept
- 2,086 canonical tournaments, awaiting live regeneration
- Method
- Generate isomorphism classes, encode every winner choice and implication, then exhaust the remaining assignments.
- Positive control
- Through three candidates, the same generator and solver return SAT; Split Cycle supplies a checked published assignment.
- Solver harness probe
- A genuine witness inside the null domain would contradict the result. Instead, the probe gives the unmodified census solver the satisfiable through-three domain and requires its SAT report count to change from exactly 0 to 1, then back to 0 when removed. Run the probe
- Result
- Bound
- The sweep stops at four candidates, uniquely weighted complete margin graphs, and the six even magnitudes shown. Claims about all voting profiles additionally require the cited projection and transfer lemma.
Move the wall.
Choose how many candidates the domain may contain. The worker constructs every signed assignment of distinct permitted margins, quotients candidate renamings, writes the constraints, and performs complete finite search.
exactly-one(T)Each tournament gets one winner, no more and no less.win(S,a) ∧ win(ab,a)If a wins before b enters and also beats b head to head…⇒ win(T,a)…binary gamma says that a must survive after b enters.
search result
Three survives. Four does not.
The candidate count is not decoration. The full finite formula is satisfiable through three candidates and unsatisfiable through four. Split Cycle is the named anchor on the satisfiable side.
Make absence earn trust.
A search that never succeeds proves nothing. These controls use the same generated domains, census solver, and rule checker as the null.
Split Cycle, through three
Not yet rerun in this session.
Swap in the SAT domain
PROBE OFF: the full through-four input has exactly 0 SAT result reports.
Allow winner sets
Computing where Split Cycle ceases to be singleton-valued…
The live evaluator checks whether the set-valued method retains binary gamma. What fails is quasi-resoluteness on uniquely weighted inputs.
Ask for candidate five
The engine refuses counts outside 2 through 4. It does not silently extrapolate the census, invent margins, or label an interrupted search UNSAT.
Names wash off.
The finite census concerns pairwise margin graphs, not raw ballots. This small instrument forms a margin graph and canonicalizes it. Relabel the candidates: the fingerprint remains fixed.
canonical margin fingerprint
This demonstrates the projection’s invariance, not the full transfer theorem. The theorem also needs a construction from weighted tournaments to profiles and a proof that the four axioms are preserved.
Why a finite obstruction matters.
The browser proves the finite weighted-tournament statement. Holliday, Norman, Pacuit and Zahedian prove the larger voting-method theorem using a separate transfer lemma. The logical dependency is explicit here.
Assume an anonymous, neutral voting method satisfies binary gamma and quasi-resoluteness for every profile with at most four candidates.
Lemma 3.6 projects that method, at a fixed maximum margin, to a pairwise method while preserving those properties.
Restrict the projected method to profiles represented by the six even margins in this census.
The restriction would produce a resolute binary-gamma assignment for all 2,086 canonical tournaments.
The complete search returns no such assignment, contradicting the assumption.
The check.
Everything labeled computed below comes from this session’s four-candidate run. The printed counts are also independently regenerated by the repository verifier.
domain…
variables…
clauses…
branches…
result…
Uncertainty and free choices
- Candidate names are quotiented by choosing the lexicographically least signed edge vector. A different canonical representative changes labels, not the isomorphism classes.
- The six even margins are a proof-generating restriction, not a model of typical elections.
- The live search is a complete finite backtracker with constraint propagation. It is independently reimplemented in the verifier, but it is not a formally checked proof trace.
- This page regenerates the full 2,086-tournament domain. It does not redistribute or claim to regenerate the paper’s deletion-produced 716-tournament subset.
- The profile widget demonstrates renaming invariance only. It does not re-prove Debord representation or Lemma 3.6.
- Past four candidates, repeated edge weights, other margin sets, and interrupted or timed-out runs are outside this certificate.