Source-linked AI summary
The Deterministic Hare Core Is Nonempty for Nine-Seat Approval Elections
Jiarui Fang
TL;DR
Deterministic Hare-quota core existence was unresolved for arbitrary committee sizes. This paper couples all blockers of one-candidate extensions through a minimal closed response system and proves that every finite nine-seat approval election has a deterministic core committee. The result settles the nine-seat case while leaving larger committee sizes open.
Problem
Deterministic Hare-quota core existence was unresolved for arbitrary committee sizes, despite prior unrestricted results through eight seats.
Method
Starting from an eight-seat PAV-maximizing core committee, the proof eliminates singleton responses, certifies PAV drift bounds, and couples the remaining responses through an irreducible stationary chain.
Results
Every finite approval election with at least nine candidates has a nine-seat deterministic Hare-quota core committee.
Takeaways & Limitations
The theorem extends deterministic core nonemptiness from k ≤8 to k ≤9 and confines unresolved instances to k ≥10, at least 16 candidates, and at least eight distinct approval types.
Takeaways & Limitations
The paper neither proves deterministic core nonemptiness for arbitrary k nor provides the corresponding larger-committee certificates.
Abstract
from arXiv · showhide
Core stability gives approval-based committee elections a strong form of coalitional proportionality, but deterministic existence is not known for an arbitrary number of seats. We prove that every finite election with nine seats has a deterministic Hare-quota core committee. Starting from an eight-seat committee that is both a global Proportional Approval Voting (PAV) maximizer and core stable, we suppose that all one-candidate extensions are blocked and extract an inclusion-minimal closed response system. Singleton responses are eliminated by exact equality rigidity. For the remaining responses, rational Farkas certificates bound every nonpositive PAV add-marginal drift below by $-n/189$ and force every successor drift above $n/126$. The uniform response chain is irreducible, so stationarity makes these bounds incompatible. The computer-assisted component comprises an exact pointwise check over 7,356 voter types, 36 one-blocker cells, and a symmetry-complete family of 19 two-blocker motifs. Exact certificate archives and standard-library verifiers support these checks. The theorem settles the nine-seat case but does not decide deterministic core existence for arbitrary committee size.
1 Introduction
Deterministic Hare-quota core existence remains unresolved in general, and this paper extends the verified unrestricted committee-size range from eight to nine. Its proof couples all possible blocker responses through a closed system and a stationary-flow contradiction.
- Motivation: Core stability requires that no coalition can use its proportional seat share to make every member strictly better off.This combines individual utility with group entitlement and is stronger than many candidate-by-candidate proportionality axioms.
- Open question: Existence of a deterministic Hare-quota core committee was previously known for at most eight seats, while unrestricted existence remained open.Prior work also established bounds based on candidate count, voter count, and distinct approval types.
- Contribution: The present theorem extends the verified unrestricted committee-size range from eight to nine.The paper includes a bounded source audit and makes no claim of an exhaustive priority search.
- Proof strategy: A one-blocker-at-a-time argument is insufficient because replacing a blocked extension can create another blocker, forming a closed response cycle.The proof therefore models all blockers in an inclusion-minimal closed system within one voter profile.
- Proof strategy: The proof eliminates singleton responses, certifies PAV drift bounds for the remaining responses, and uses an irreducible Markov chain whose stationary mean yields a contradiction.The release includes symbolic reductions, certificate formats, exact verifiers, and the trusted-computing-base boundary.
2 Model and theorem
The paper formalizes approval elections, coalitional blocking, and Hare-core stability through an exact integer condition, then states deterministic nonemptiness for nine-seat committees.
- Model: An election consists of a finite voter set, a finite candidate set, and approval sets, with n denoting the number of voters.Committees are fixed-size subsets of candidates.
- Blocking: A coalition blocks a committee through an affordable target when every coalition member strictly prefers the target to the committee.Targets may overlap the current committee, and equality in the affordability condition is allowed.
- Blocking: A target blocks a committee exactly when kq(W,T) < n|T| for some nonempty target T with |T| ≤ k.This integer characterization avoids rounding and ceiling conventions.
- Theorem: The paper presents an exact deterministic existence theorem for nine-seat committees.The theorem applies to every finite approval election with at least nine candidates and guarantees a nine-member set satisfying the core condition for every nonempty target of size at most nine.
3 The certified eight-seat anchor
The proof begins from an eight-seat committee that is both a global PAV maximizer and Hare-core stable, then studies exact PAV gains from adding an outsider.
- Anchor theorem: Peters’s theorem guarantees that some global PAV maximizer among eight-element committees is an eight-seat Hare-core committee.The source theorem uses rational certificates rather than floating-point feasibility tolerances.
- Anchor theorem: The anchor theorem remains applicable with repeated approval types and empty ballots after the stated preprocessing and reinsertion argument.If every ballot is empty, every committee is core.
- Extension analysis: For an eight-set U and outsider c, the extension W_c = U ∪{c} is analyzed through its exact PAV add marginal.The add marginal is a_c = Φ(U ∪{c}) − Φ(U).
4 Blockers as a closed response system
Blocked nine-seat extensions are organized into a minimal closed response system, whose response graph is irreducible and therefore suitable for the later stationary-flow argument.
- Response construction: If a target blocks W_c, it excludes c, has a nonempty response set outside U, and cannot block the corresponding extension after replacing c by a response outsider.These conclusions follow by cancellation against the eight-seat core U.
- Closed systems: A closed fixed-U blocker system assigns each outsider c a blocker whose response set stays inside the system.If every extension is blocked, the full outsider set forms such a system, and finiteness supplies an inclusion-minimal one.
- Irreducibility: The response digraph of an inclusion-minimal closed system is strongly connected.Otherwise, a sink strongly connected component would itself be a smaller closed system, contradicting minimality.
5 Singleton responses cannot occur in a closed system
Exact equality rigidity eliminates singleton responses from any closed fixed-U blocker system, so every internal response must contain at least two outsiders. The proof combines voter-type certificates with tied-swap arguments and rules out consecutive singleton responses.
- Equality rigidity: Singleton rigidity characterizes gainers and forces every swap U −u + x to tie the global PAV maximizer.The characterization separates gainers approving x from nongainers and makes the aggregate swap changes compatible with equality in the PAV bounds.
- Response classification: A bare outsider singleton is the only remaining possible blocker after tied-candidate absorption.For h ≥1 or for at least two outsiders, the certified bounds exclude blocking; the h = 0, r = 1 case is the sole surviving case.
- Equality rigidity: Exact pointwise certificates average voter types by approval counts and convert strict-gainer indicators into PAV-change inequalities.The verifier checks all 6,384 middle types, 936 empty-H types, and 36 h = 8 types using exact rational arithmetic.
- Response classification: No two singleton responses can occur in succession, because the second gainer set would contradict the first block’s tied-swap partition.The contradiction applies both to interior cases and to the h′ = 0 and h′ = 8 boundary cases.
- Response classification: Every internal blocker in a closed fixed-U system therefore has at least two outsiders.A singleton internal blocker would force a singleton response, which the preceding rigidity and succession lemmas prohibit.
6 One-blocker PAV drift
The one-blocker analysis assigns an exact PAV add-marginal drift to each blocker cell and certifies bounds across all 36 feasible (h, r) cells. Nonpositive drift is confined to a small set of cells, while larger outsider sets force positive drift.
- Drift theorem: Lemma 6.1 gives exact lower bounds on normalized add-marginal drift for every blocker with at least two outsiders.The analysis averages voter orbits and combines one-swap PAV rows, the weak core row, competitor rows, and the exact blocking row.
- Drift bounds: If δc ≤0, then the blocker must contain committee members and exactly two or three outsiders.This follows immediately from the positive lower bounds in the r = 0 and r ≥4 regions.
- Drift theorem: The certified drift table covers all 36 pairs with h ≥0, r ≥2, and h+r ≤9.Each cell is supported by nonnegative rational Farkas multipliers and an exact rational verifier.
- Drift bounds: −1/189 is the minimum normalized drift for r ≤3, while the minimum for r ≥4 is 1/126.The only negative cells are (2,2), (3,2), and (2,3); zero cells are (1,2), (4,2), and (3,3).
7 The simultaneous two-blocker separation
The simultaneous two-blocker analysis rules out the local configurations needed to sustain nonpositive drift in a closed response system. Exact symmetry-complete Farkas certificates cover 19 response motifs and show that the relevant blocker pairs cannot coexist.
- Simultaneous separation: Two-blocker separation is necessary because separately feasible local blocker analyses do not capture simultaneous feasibility in one voter profile.The proof therefore models two blockers together using shared voter-orbit masses and a common block scale.
- Two-outsider sources: For source responses with two outsiders, eight response motifs are checked across every ordered Venn pattern of their committee-member sets.The exact archive proves that the two blocks cannot coexist when the source drift is nonpositive.
- Three-outsider sources: For source responses with three outsiders, five motifs for rx = 2 and six for rx = 3 cover all admissible successor structures.The source drift restriction reduces hc to 2 or 3, and the archive covers all 427 resulting Venn orbits.
- Farkas separation: The certificate system forces the common block scale z below one, contradicting the normalized assumption z = 1.Nonnegative multipliers satisfy λ^Tα ≥1 and produce β <1 for every voter orbit.
- Farkas separation: The two exact packages exhaust 19 motifs, including mutual edges, back edges, shared response candidates, and wholly fresh responses.A builder-independent checker also verifies the response-set permutation action and the 1,008 + 427 Venn-cell count.
8 Stationary-flow contradiction
The proof couples all blocked extensions into an irreducible response system and applies stationary flow to certified PAV drifts. Uniform lower and successor-gain bounds make stationarity impossible, so some nine-seat extension is core stable.
- Lemma 8.1 shows that an irreducible chain cannot combine a uniform drift loss bound with strictly larger drift at every successor of a nonpositive-drift state.
- The proof assumes every eight-seat extension is blocked, then selects an inclusion-minimal closed system with one internal blocker per state.
- The response digraph is strongly connected, yielding an irreducible stochastic matrix with a positive stationary distribution.
- Here, nonpositive states have drift at least −n/189, while every relevant successor has drift at least n/126.
- Stationarity telescopes the PAV marginals, and the resulting positive stationary mean contradicts the zero stationary mean, proving that some Wc is a nine-seat core.
- The argument covers target sizes one through nine, allows overlap with the committee, and treats quota equality as blocking.
9 Computer-assisted proof boundary and validation
The computer-assisted proof validates frozen rational certificates with exact, standard-library verifiers that reconstruct the relevant finite voter-orbit checks. The validation establishes certificate correctness and source compilability, not certificate generation or full replay of every external dependency.
- The trusted base includes symbolic proof components, exact finite verification, arbitrary-precision rational arithmetic, frozen certificate datasets, and row-reconstructing verifiers.
- The package validates three frozen certificate archives but does not regenerate them, provide solver logs, or replay the external certificate underlying Theorem 3.1.
- The released checks include motif coverage, tied-candidate absorption, general blocker drift, and directed r2 and r3 edge verification.
- Each verifier reconstructs voter orbits, strict-gainer predicates, PAV inequalities, and Farkas signs before checking stored rational multipliers.
- 9.1 Two worked certificate records: The one-blocker example uses 54 exact voter orbits and checks a certificate inequality on every orbit.
- 9.1 Two worked certificate records: The two-blocker motif uses 128 ballot orbits, with verifier rows encoding an averaged PAV inequality and two scaled blocking inequalities.
- 9.1 Two worked certificate records: For the worked two-blocker motif, the common-scale coefficient is 1 while the resulting bound is β = 8/9 < 1.
10 Discussion and conclusion
The paper proves deterministic Hare-core nonemptiness for nine-seat approval elections, extending the known guarantee through k ≤9. Its certificates and equality analysis remain specific to the eight-to-nine extension, so arbitrary-seat existence remains unresolved.
- Theorem 2.2 establishes deterministic Hare-core nonemptiness at k = 9, and together with prior results gives nonemptiness for every k ≤9.
- The unresolved region is confined to k ≥10, at least 16 candidates, and at least eight distinct approval types.
- The closure argument is reusable at another seat number only if uniform one-blocker loss and successor-gain certificates satisfy M > L.
- The eight-to-nine constants and equality analysis do not themselves provide certificates for larger committees.
- The paper neither proves nonemptiness for arbitrary k nor supplies an empty-core election, and makes no polynomial-time claim for finding the certified anchor or stable extension.
AI use disclosure
The paper discloses AI assistance in proof exploration, verifier development, literature-query formulation, drafting, and release packaging. It states that mathematical evidence comes from the symbolic proof, frozen exact certificates, and independently replayable verifiers, with the author retaining responsibility.
- OpenAI Codex using GPT-5.6 Sol assisted with proof exploration, exact-verifier development, literature-query formulation, manuscript drafting, and release packaging.
- AI-generated output is not treated as mathematical evidence; support comes from the symbolic proof, frozen exact rational certificates, and independently replayable verifiers.
- The author reviewed the statements, proofs, citations, source code, and final artifacts and remains responsible for the result.