Answer: Polynomial-time constructible, in \(\mathrm{FP}\), including the entire encoded derivation.
Theorem 2 — class: algorithmic
PDF text-layer excerpt — equations and symbol order may be approximateFor any given profile, Borda-expl computes a proof justifying the outcome of the Borda rule in terms of the ℒ-axiomatisation 𝐽𝐵.
statement extracted from the paper’s text layer; consult the paper for the exact wording
Given a finite alternative set \(C\) and a binary-rational distribution \(\mu\) over \(\tau\) complete rankings, construct a finite derivation of \(W(\mu)=\arg\max_{c\in C}\sum_t\mu_t s(t,c)\) from a rational-mass extension of \(J_B\). Intermediate profiles are finite nonzero rational measures over rankings, with the paper’s \(\mathrm{Elem}\), \(\mathrm{Cycl}\), \(\mathrm{Canc}\), and reinforcement axioms interpreted on those measures.
Let \(C\) be a nonempty alternative set, \(m=|C|\), with a fixed reference order. Types are strict complete rankings. A society is given by its support: the list of the \(\tau\) types with positive mass, each mass a binary rational; \(\tau\) is the support size, not the number of possible rankings. The input \(\mu\) has total mass \(1\); let \(L\) be its total input bit length.
Intermediate profiles \(P\) are finite nonzero nonnegative rational measures over rankings, without normalization; addition and positive rational scaling act on masses. All profiles appearing in proofs are encoded explicitly by support and binary-rational masses.
An atom \([P\mapsto A]\), for \(\varnothing\ne A\subseteq C\), asserts that the complete winner set is \(A\). Background axioms require exactly one such set for each profile; derivations use classical propositional natural deduction, with earlier lines reusable.
For each nonempty \(A\subseteq C\), let \(E_A\) assign unit mass to the ranking listing \(A\) then \(C\setminus A\) in reference order, and to the ranking reversing both blocks while keeping \(A\) first. Coincident rankings have their masses added. For each cycle \(S\) visiting every alternative once, let \(D_S\) assign unit mass to each cyclic rotation of its ranking.
The rational-mass axiom system \(J_B^{\mathbb Q}\) contains \(\mathrm{Elem}: [qE_A\mapsto A]\) and \(\mathrm{Cycl}: [qD_S\mapsto C]\) for every \(q\in\mathbb Q_{>0}\); \(\mathrm{Canc}: [P\mapsto C]\) whenever, for every distinct pair, the mass preferring either alternative to the other is equal.
It also contains \(\mathrm{Reinf}: ([P\mapsto A]\land[Q\mapsto B])\to[P+Q\mapsto A\cap B]\) when \(A\cap B\ne\varnothing\); \(\mathrm{Reinf\text{-}sub}: ([P+Q\mapsto A]\land[Q\mapsto C])\to[P\mapsto A]\); and \(\mathrm{Simp}: [qP\mapsto A]\to[P\mapsto A]\) for \(q\in\mathbb Q_{>0}\).
The computational task is to construct a finite derivation of \([\mu\mapsto W(\mu)]\) from these axioms and the background axioms, where \(W(\mu)=\operatorname*{arg\,max}_{c\in C}\sum_t\mu_t s(t,c)\), \(s\) is the standard Borda score, and all tied maximizers are included.
Can this derivation be constructed in time polynomial in \(m,\tau,L\), counting the entire encoded output, or is this search problem NP-hard?
For finite electorates, Cailloux and Endriss give an algorithm constructing Borda justifications from the six discrete axioms, without an explicit polynomial-time bound ([source](https://eprints.illc.uva.nl/id/eprint/552/)). Peters et al. prove an \(O(m^2)\) bound on explanation steps for discrete profiles using these axioms plus a multiplication shortcut ([source](https://zixinzhou.com/pdf/explain.pdf)).
No result settling the stated rational-mass proof-generation problem was located.
The derivation can be constructed in time polynomial in \(m,\tau,L\), including the entire encoded output. In fact, \(O(m^2)\) natural-deduction lines suffice, with polynomially bounded support sizes and rational bit lengths.
The construction uses the pairwise-margin viewpoint of [Peters et al., Appendix C.1](https://zixinzhou.com/pdf/explain.pdf). Below, an explicit identity supplies the required cyclic profiles, and the encoding bounds are proved directly.
Index alternatives by their fixed reference order. For any profile \(P\), write \(n(P)\) for its total mass and define the antisymmetric margin matrix by
\[ \delta(P)_{ab} = \sum_{t:a\succ_t b}P_t-\sum_{t:b\succ_t a}P_t, \qquad \delta(P)_{aa}=0. \]
Define its row sums by \(\beta(P)_a=\sum_{b\ne a}\delta(P)_{ab}\). If \(b(P)_a\) denotes the Borda score of \(a\), then
\[ \beta(P)_a=2b(P)_a-(m-1)n(P). \]
Indeed, the Borda score counts, for each other alternative, the mass ranking \(a\) above that alternative. The two directional masses for each pair sum to \(n(P)\). Consequently, maximizing \(\beta(P)\) gives exactly the complete Borda winner set.
Both \(\delta\) and \(\beta\) are additive and rational-linear. Antisymmetry also gives \(\sum_a\beta(P)_a=0\).
If \(m=1\), cancellation applies vacuously to \(\mu\), proving \([\mu\mapsto C]\). Henceforth assume \(m\ge 2\).
Lemma. Given nonzero profiles \(R,M\) with \(\delta(R)=\delta(M)\), a derivation of \([R\mapsto A]\) can be extended by a constant number of lines to derive \([M\mapsto A]\).
Proof. Let \(\overline R\) reverse every ranking of \(R\), preserving its mass. Then \(\delta(\overline R)=-\delta(R)\). Define
\[ U=M+\overline R, \qquad V=R+\overline R. \]
Both have zero margins. Cancellation therefore supplies \([U\mapsto C]\) and \([V\mapsto C]\).
Reinforcement applied to \([R\mapsto A]\) and \([U\mapsto C]\) gives \([R+U\mapsto A]\). As measures,
\[ R+U=M+V. \]
Thus reinforcement-subtraction, using \([V\mapsto C]\), gives \([M\mapsto A]\).
Each reinforcement application expands into its axiom instance, conjunction introduction, and implication elimination. All profiles are nonzero and nonnegative. When supports are aggregated and canonically ordered, \(R+U\) and \(M+V\) have identical encodings; no additional equality principle is needed. \(\square\)
Put \(\beta_a=\beta(\mu)_a\), and order the alternatives as \(a_1,\ldots,a_m\) so that
\[ \beta_{a_1}\ge\beta_{a_2}\ge\cdots\ge\beta_{a_m}. \]
For \(1\le k<m\), define \(A_k=\{a_1,\ldots,a_k\}\) and
\[ q_k=\frac{\beta_{a_k}-\beta_{a_{k+1}}}{2m}. \]
These coefficients are nonnegative. Form the nonzero profile
\[ E=E_C+\sum_{\substack{1\le k<m\\q_k>0}}q_kE_{A_k}. \]
The rankings defining every \(E_{A_k}\) use the prescribed reference order.
For a subset \(A\) of size \(k\), the two rankings in \(E_A\) give zero margins within each block and margin \(2\) from every member of \(A\) to every member of its complement. Therefore
\[ \beta(E_A)_a= \begin{cases} 2(m-k),&a\in A,\\ -2k,&a\notin A. \end{cases} \]
In particular, \(\delta(E_C)=0\). Between consecutive alternatives in the score order, only the cut \(A_k\) separates \(a_k\) and \(a_{k+1}\). Hence
\[ \beta(E)_{a_k}-\beta(E)_{a_{k+1}} = 2mq_k = \beta_{a_k}-\beta_{a_{k+1}}. \]
Thus \(\beta(E)-\beta(\mu)\) is constant across alternatives. Both vectors sum to zero, so
\[ \beta(E)=\beta(\mu). \]
The winner set of \(E\) is formally derivable without assuming this equality. Elem supplies \([E_C\mapsto C]\) and, for each positive coefficient, \([q_kE_{A_k}\mapsto A_k]\). Reinforcement combines them.
If every coefficient is zero, all Borda scores tie and the resulting set is \(C=W(\mu)\). Otherwise, let \(k_0\) be the first index with \(q_{k_0}>0\). The positive-coefficient sets are nested, and their intersection is \(A_{k_0}\), precisely the set of all tied maximizers. Every intermediate intersection is nonempty. We therefore obtain
\[ [E\mapsto W(\mu)] \]
in \(O(m)\) proof lines.
Set \(x=\delta(\mu)-\delta(E)\). The preceding section proves that every row sum of \(x\) is zero. We now construct a nonzero profile \(T\) with
\[ \delta(T)=x, \qquad [T\mapsto C] \]
derivable in \(O(m^2)\) lines.
For an antisymmetric matrix \(z\), let \(d_a(z)=\sum_bz_{ab}\), and define
\[ (\Pi z)_{ab}=z_{ab}-\frac{d_a(z)-d_b(z)}m. \]
Antisymmetry implies \(\sum_ad_a(z)=0\). Consequently,
\[ \sum_b(\Pi z)_{ab} = d_a(z)-\frac{md_a(z)-\sum_bd_b(z)}m = 0. \]
Moreover, if \(z\) already has zero row sums, then \(\Pi z=z\).
For reference-ordered indices \(i<j\), let \(e^{ij}\) have entry \(1\) at \((i,j)\), entry \(-1\) at \((j,i)\), and zero elsewhere. Thus every antisymmetric matrix satisfies
\[ z=\sum_{i<j}z_{ij}e^{ij}. \]
For a ranking \(r\), let \(\varepsilon(r)\) be its unit-mass margin matrix and \(p_r(a)\) the position of \(a\), numbered from \(1\). Then
\[ d_a(\varepsilon(r))=m+1-2p_r(a). \]
Write \(D_r\) for the cyclic profile generated by the ranking \(r\). If \(a\) precedes \(b\) and their positional distance is \(d\), exactly \(m-d\) rotations rank \(a\) above \(b\), while \(d\) rank \(b\) above \(a\). Applying this observation in both positional orders gives
\[ \delta(D_r)_{ab} = m\varepsilon(r)_{ab} + 2\bigl(p_r(a)-p_r(b)\bigr). \]
Combining the last two identities yields
\[ \delta(D_r)=m\Pi\varepsilon(r). \]
For each \(i<j\), choose \(r_{ij}\) to list \(i,j\) first, followed by the remaining alternatives in reference order. Let \(r'_{ij}\) exchange its first two alternatives. Because they are adjacent, only their mutual comparison changes:
\[ \varepsilon(r_{ij})-\varepsilon(r'_{ij})=2e^{ij}. \]
Therefore
\[ \delta(D_{r_{ij}})-\delta(D_{r'_{ij}}) = 2m\Pi e^{ij}. \]
Since \(x\) has zero row sums, linearity now proves the explicit decomposition
\[ x = \sum_{i<j} \frac{x_{ij}}{2m} \left( \delta(D_{r_{ij}})-\delta(D_{r'_{ij}}) \right). \]
Reversing every ranking in a cyclic profile produces another cyclic profile and negates its margins.
For each pair with \(x_{ij}\ne0\), set \(\alpha_{ij}=|x_{ij}|/(2m)>0\). Define \(T_{ij}\) as follows:
In both cases its margin matrix is the corresponding summand in the decomposition. Define
\[ T=E_C+\sum_{\substack{i<j\\x_{ij}\ne0}}T_{ij}. \]
Then \(T\) is nonzero and \(\delta(T)=x\). Elem proves the full winner set for the initial \(E_C\). Cycl proves the full winner set for each positively scaled cyclic summand. Repeated reinforcement therefore proves \([T\mapsto C]\).
There are at most \(2\binom m2\) cyclic summands, so this takes \(O(m^2)\) lines. No signed measure is used as a profile.
Let \(H=E+T\). Reinforcement gives \([H\mapsto W(\mu)]\), and
\[ \delta(H) = \delta(E)+\delta(T) = \delta(\mu). \]
The transfer lemma, with \(R=H\) and \(M=\mu\), completes the derivation of
\[ [\mu\mapsto W(\mu)]. \]
The construction uses only Elem, Cycl, Canc, Reinf, and Reinf-sub. It requires neither Simp nor the background uniqueness axioms.
We bound both support sizes and rational bit lengths.
The profile \(E\) contains at most \(m\) elementary summands, each supported on at most two rankings. The profile \(T\) contains at most \(2\binom m2\) cyclic summands, each supported on \(m\) rankings, plus \(E_C\). Thus
\[ |\operatorname{supp}(H)|=O(m^3). \]
Reversal preserves support size, and addition takes unions of supports. Every profile in the construction and transfer therefore has support size \(O(\tau+m^3)\).
There are \(O(m^2)\) proof lines. Every axiom instance and logical inference used contains only a constant number of atoms, even when every profile occurrence is encoded in full.
Write the input masses as \(p_t/d_t\), with positive integer denominators, and let \(D=\prod_td_t\). The binary length of \(D\) is \(O(L)\).
Every input margin and row sum has denominator dividing \(D\). Consequently:
All masses in every constructed profile can therefore be represented over the single denominator \(B=2m^2D\). Additions and reversals introduce no larger denominator.
It remains to bound the numerators. Because \(\mu\) has total mass \(1\), \(|\delta(\mu)_{ab}|\le1\) and \(|\beta_a|\le m-1\). Telescoping gives
\[ \sum_{k=1}^{m-1}q_k = \frac{\beta_{a_1}-\beta_{a_m}}{2m} \le\frac{m-1}{m}<1. \]
Thus \(n(E)<4\). The initial \(E_C\) has zero margins, so \(|\delta(E)_{ab}|<2\), whence \(|x_{ab}|<3\).
Each pair contributes two cyclic profiles, giving total mass \(2m\alpha_{ij}=|x_{ij}|<3\). Hence
\[ n(T)\le2+3\binom m2, \qquad n(H)<6+3\binom m2. \]
All transfer profiles also have total mass \(O(m^2)\). Every individual mass consequently has numerator at most \(O(m^2)B\), and its complete rational encoding uses \(O(L+\log m)\) bits.
After indexing alternatives by reference order, a ranking uses \(O(m\log m)\) bits. The entire expanded proof therefore has size
\[ O\!\left( m^2(\tau+m^3) \bigl(m\log m+L+\log m\bigr) \right). \]
Computing margins, sorting row sums, generating the specified rankings, performing the rational arithmetic, aggregating supports, and printing the proof all require polynomial time: their counts and operand bit lengths are polynomially bounded as above.
This proves polynomial-time construction with the full output counted.
⟨structured verdict parsed — rendered above⟩
Verdict: proved. The output establishes polynomial-time construction of the requested derivation, including its full explicit encoding. I found no major or minor mathematical issues.
The construction addresses the stated rational-mass system directly. It does not merely bound the number of explanation steps: it also bounds the supports and rational bit lengths of all profiles appearing in those steps.
The identity
\( \beta(P)_a=2b(P)_a-(m-1)n(P) \)
is correct for standard Borda scores. For each opponent, the two directional comparison masses sum to \(n(P)\), so summing their differences gives the displayed formula.
Consequently, maximizing \(\beta(P)\) preserves the complete Borda winner set, including all ties. Additivity, rational linearity, and the zero sum of the row sums all follow from the definition of the antisymmetric margin matrix.
The case \(m=1\) is correctly handled: cancellation has no pairwise conditions to check, and the sole alternative is the Borda winner.
Assessment: correct, including the boundary case.
Every step of the transfer lemma is valid:
All these profiles are nonzero nonnegative rational measures. Canonical aggregation and ordering of supports makes the two encodings of the combined measure identical, so the argument does not assume an unavailable equality rule.
The specified expansion into axiom instances, conjunction introduction, and implication elimination requires only a constant number of natural-deduction lines.
Assessment: correct and formally compatible with the stated proof system.
The elementary-profile margin calculation is correct. Reversing both blocks cancels every comparison within a block, while every cross-block comparison favors the member of \(A\) in both rankings. This yields precisely the stated row sums.
The coefficients \(q_k\) are nonnegative because the alternatives are sorted by decreasing \(\beta_a\). Zero coefficients are omitted, so every scaled profile used in an Elem instance has a strictly positive scaling parameter.
For consecutive alternatives \(a_k,a_{k+1}\), every cut other than \(A_k\) puts them in the same block. The difference between their row sums contributed by \(E_{A_k}\) is \(2m\). Hence the consecutive differences of \(\beta(E)\) agree with those of \(\beta(\mu)\). Their zero total sums then establish the claimed equality.
The winner-set derivation also checks out independently:
Coincident rankings cause no problem because their masses are aggregated as required by the task.
Assessment: correct; ties and the all-tied case are fully addressed.
The map \(\Pi\) preserves antisymmetry and has zero row sums. The calculation uses \(\sum_a d_a(z)=0\), which is valid for every antisymmetric matrix.
For matrices already having zero row sums, \(\Pi z=z\). The matrices \(e^{ij}\) give the stated coordinate expansion of an arbitrary antisymmetric matrix.
Since \(\beta(E)=\beta(\mu)\), the residual matrix \(x\) does indeed have zero row sums.
Assessment: correct.
The rotation count is correct. When \(a\) precedes \(b\) at positional distance \(d\), exactly \(m-d\) rotations preserve that comparison and \(d\) reverse it. Thus the resulting margin is \(m-2d\), agreeing with the stated formula.
The ranking row-sum identity
\(d_a(\varepsilon(r))=m+1-2p_r(a)\)
is also correct. Substitution gives
\(\delta(D_r)=m\Pi\varepsilon(r)\)
with the stated sign and factor.
Swapping the adjacent first two alternatives changes only their mutual comparison. Therefore the difference of unit-ranking margin matrices is \(2e^{ij}\), and the cyclic-profile difference is \(2m\Pi e^{ij}\).
Applying these identities to the coordinate expansion of \(x\), with \(\Pi x=x\), establishes the displayed decomposition. There is no unstated spanning assumption.
Assessment: correct; all critical constants and signs check.
Reversal takes the rotations of a ranking to the rotations of its reversed ranking, so the reversed profile remains a Cycl profile and has negated margins.
The two sign cases defining \(T_{ij}\) realize exactly the corresponding signed summand of the decomposition using positive masses. Signed matrices are used for computation, but no signed measure appears as a proof profile.
Adding \(E_C\) ensures that \(T\) remains nonzero even when \(x=0\). Every scaled cyclic summand has a positive rational coefficient and hence is licensed by Cycl. Reinforcement always intersects \(C\) with \(C\).
For \(m=2\), zero row sums force the sole independent residual entry to vanish. Thus this boundary case correctly uses only the initial \(E_C\).
Assessment: correct, including zero residuals and small alternative sets.
Reinforcement applies to \(E\) and \(T\), giving \(H\) the complete winner set \(W(\mu)\). Their margin identity gives \(\delta(H)=\delta(\mu)\), so the verified transfer lemma yields the requested atom.
The construction genuinely uses only Elem, Cycl, Canc, Reinf, and Reinf-sub. Positive rational scaling is licensed directly by Elem and Cycl; no multiplication shortcut or reverse use of Simp is assumed.
The reference to [Peters et al., Appendix C.1](https://zixinzhou.com/pdf/explain.pdf) supplies context for the margin approach. The output proves the identities and transfer argument it needs, rather than relying on an external discrete theorem to establish the rational-mass result.
Assessment: the requested derivation is established.
There are at most \(m\) elementary summands and \(2\binom m2\) cyclic summands. Their stated support bounds yield \(|\operatorname{supp}(H)|=O(m^3)\).
Intermediate partial sums use subsets of those supports. Reversal preserves support size, and the transfer construction only adds unions with the input support. Consequently, every proof profile has support size \(O(\tau+m^3)\).
Each reinforcement application expands into a constant number of logical lines. The resulting \(O(m^2)\) bound therefore counts natural-deduction lines, not merely informal explanation operations.
Assessment: correct.
The denominator bounds check:
Thus the proposed common denominator \(B=2m^2D\) accommodates every constructed mass. Its binary length is \(O(L+\log m)\); its potentially large numerical value does not invalidate the bit-length bound.
The total-mass estimates are also correct:
These estimates justify the claimed \(O(L+\log m)\) bit length of each individual rational mass.
Assessment: correct.
The final output-size bound accounts for explicitly written rankings and masses at every profile occurrence. Winner-set encodings and line references fit within the stated bound.
The listed operations—exact margin computation, rational comparisons, ranking generation, support aggregation, and printing—have polynomially many operations on polynomial-length operands. The argument therefore establishes polynomial running time as well as polynomial output size.
Assessment: the complexity claim is justified.
No repair or additional clarification is needed to make the argument verifiable. The output resolves the assigned rational-mass proof-generation problem.
⟨structured verdict parsed — rendered above⟩
Tier: machine-proved, adversarially reviewed by an independent model. No human has checked this proof. Generated from pipeline artifacts by tools/atlas_build.py.