← back to the atlas

d4-conf-atal-2016-0079 (d4-conf-atal-2016-0079)

Answer: All limits exist, and exact computation is polynomial-time solvable: \(O(m+\tau)\) arithmetic operations and \(O((m+\tau)L^2)\) bit operations for a standard explicit input encoding.

The anchor (named result in the paper)

Theorem 6 — class: algorithmic

PDF text-layer excerpt — equations and symbol order may be approximateWeights under mechanism LEGIT+ can be computed in O(|V | + |E|) time. 5.

statement extracted from the paper’s text layer; consult the paper for the exact wording

The continuous mirror question, as graded

Given a finite rooted connector tree \(H\), a map \(h\) from supported voter types \(t\) to connectors, and rational masses \(\mu_t>0\) summing to \(1\), form, for each denominator-compatible \(N\), a network by attaching \(N\mu_t\) voter leaves of type \(t\) to \(h(t)\), with the root as target. For each type \(t\), compute the exact limit \(q_t=\lim_{N\to\infty}Nw_v^{(N)}\), where \(w_v^{(N)}\) is the LEGIT+ weight of any type-\(t\) voter in that expansion; equivalently, compute each type’s total weight \(\alpha_t=\mu_tq_t\).

Packaged proof task (what the prover saw — nothing else)

Let \(H\) be a finite undirected rooted tree with \(m\geq1\) connector vertices and root \(r\); all connectors, including \(r\), are non-voters.
A society is given by its support: the list of \(\tau\geq1\) types with positive mass, each mass \(\mu_t\) a binary rational, with \(\sum_t\mu_t=1\). Here \(\tau\) is the support size, not the number of possible types. The input also specifies \(h(t)\in V(H)\); let \(L\) be the total input bit length.
For each positive integer \(N\) satisfying \(N\mu_t\in\mathbb Z\) for every supported type, form \(G_N\) by attaching \(N\mu_t\) distinct voter leaves of type \(t\) to \(h(t)\). Root the expanded tree at \(r\).
On a rooted tree, LEGIT+ starts with weight \(1\) at the root. Each non-voter divides its incoming weight equally among its children whose descendant subtrees, including those children, contain a voter; children with no such voter receive zero. Each voter retains its incoming weight. Thus voter weights are nonnegative and sum to \(1\); opinions and type labels do not affect the rule.
Write \(w_t^{(N)}\) for the weight of any type-\(t\) leaf, and define \(q_t=\lim_{N\to\infty,\;N\mu_s\in\mathbb Z\;\forall s}Nw_t^{(N)}\), when this limit exists, and \(\alpha_t=\mu_tq_t\).

Do all these limits exist, and is their exact computation (equivalently, computation of all \(\alpha_t\)) in \(\mathrm P\) or \(\mathrm{NP}\)-hard? State running times in \(m\), \(\tau\), and \(L\).

For finite explicitly listed networks, LEGIT+ weights are computable in \(O(|V|+|E|)\) time ([Brill, Conitzer, Freeman, and Shah](https://www.cs.cmu.edu/~conitzer/FNPrecAAMAS16full.pdf)). No result settling this precise continuous limit problem was located in the literature search.

Modeling choices made when packaging the task

Prover output (gpt-6.1-sol / high, Bolzano prover prompt)

1. Result

All limits exist, and their exact computation is polynomial-time solvable. For a standard explicit encoding of the connector tree, all \(q_t\) and \(\alpha_t\) can be computed using \(O(m+\tau)\) arithmetic operations and \(O((m+\tau)L^2)\) bit operations.

Only types attached at a vertex with no positive-mass attachment at a strict ancestor receive positive limiting weight.

2. Definitions and exact finite-population weights

Root \(H\) at \(r\). For each connector \(v\), define its local mass by

\( \displaystyle a_v=\sum_{t:\,h(t)=v}\mu_t. \)

Call \(v\) *active* if its connector subtree contains a vertex with positive local mass. Define

\( \displaystyle k_v=\bigl|\{c:\ c\text{ is a connector child of }v\text{ and }c\text{ is active}\}\bigr|. \)

Activity is independent of the admissible population size \(N\): every supported type has positive mass, so its integer count \(N\mu_t\) is positive.

At connector \(v\), there are exactly \(Na_v\) directly attached voter children and \(k_v\) active connector children. Consequently, LEGIT+ divides its incoming weight into \(Na_v+k_v\) equal shares.

Fix a supported type \(t\), let \(v=h(t)\), and let \(A(v)\) denote the strict connector ancestors of \(v\). Every connector on the root-to-\(v\) path is active. Applying the division rule along this path, including the final division to a voter leaf, gives

\( \displaystyle w_t^{(N)} =\frac{1}{Na_v+k_v} \prod_{u\in A(v)}\frac{1}{Na_u+k_u}. \)

Every denominator in this formula is positive. Indeed, \(a_v>0\); and any strict ancestor \(u\) has an active connector child on the path to \(v\), so \(k_u\geq1\). All type-\(t\) leaves receive the same weight because they have the same parent and that parent divides equally among its eligible children.

3. Existence and explicit limit formula

Multiplying the preceding identity by \(N\) yields

\( \displaystyle Nw_t^{(N)} =\frac{N}{Na_v+k_v} \prod_{u\in A(v)}\frac{1}{Na_u+k_u}. \)

The first factor converges to \(1/a_v\). Each ancestor factor has a limit:

These are finitely many factors, all with finite limits. Hence their product converges along all admissible \(N\).

Define the set of first occupied vertices by

\( \displaystyle F=\{v:\ a_v>0\text{ and }a_u=0\text{ for every }u\in A(v)\}. \)

For \(v\in F\), put

\( \displaystyle P_v=\prod_{u\in A(v)}k_u, \)

where an empty product equals \(1\). The limit formula is therefore:

\( \displaystyle q_t=\frac{1}{a_{h(t)}P_{h(t)}}, \qquad \alpha_t=\frac{\mu_t}{a_{h(t)}P_{h(t)}}. \)

There are arbitrarily large admissible population sizes: writing \(\mu_t=p_t/d_t\), every positive multiple of \(\prod_t d_t\) is admissible. Thus the limiting domain is unbounded, and the argument proves precisely the limits requested.

For completeness, the limiting aggregate weights retain normalization. At every admissible \(N\),

\( \displaystyle \sum_{t=1}^{\tau}N\mu_t w_t^{(N)}=1. \)

Since \(\tau\) is finite and each summand converges, taking limits gives

\( \displaystyle \sum_{t=1}^{\tau}\alpha_t=1. \)

4. Exact algorithm and bit complexity

Represent each input mass as \(\mu_t=p_t/d_t\), with positive binary-encoded integers. Compute

\( \displaystyle D=\prod_{t=1}^{\tau}d_t,\qquad b_t=p_t(D/d_t),\qquad B_v=\sum_{t:\,h(t)=v}b_t. \)

Then \(a_v=B_v/D\). The algorithm proceeds as follows.

\( \displaystyle q_t=\frac{D}{B_{h(t)}P_{h(t)}}, \qquad \alpha_t=\frac{b_t}{B_{h(t)}P_{h(t)}}. \)

Otherwise output zero.

The Boolean for a child is true exactly when its parent has positive local mass or the parent’s Boolean is already true. Thus step 4 implements the proved formula.

There are \(O(m+\tau)\) graph operations and integer arithmetic operations. To bound their bit cost, observe:

\( \displaystyle \log_2P_v =\sum_{u\in A(v)}\log_2k_u \leq\sum_{u\in A(v)}k_u \leq m-1. \)

The last inequality holds because the connector tree has \(m-1\) edges and \(\sum_u k_u\leq m-1\).

Consequently, every intermediate integer and output numerator or denominator has \(O(L+m)\) bits. Schoolbook integer arithmetic gives the conservative bound

\( \displaystyle O\!\left(L+(m+\tau)(L+m)^2\right) \)

bit operations. Reduced output fractions, if required, can be obtained within the same bound using quadratic-time gcd computation. For a standard explicit tree encoding, \(m=O(L)\), so this simplifies to \(O((m+\tau)L^2)\). The total output length is \(O(\tau(L+m))\).

The finite-network linear-time theorem in [Brill, Conitzer, Freeman, and Shah, Theorem 6](https://www.cs.cmu.edu/~conitzer/FNPrecAAMAS16full.pdf) concerns explicitly listed networks. The bounds above compute the limits directly from the supported types and connector tree.

⟨structured verdict parsed — rendered above⟩

Adversarial review (gpt-6.1-sol / medium, Bolzano verifier prompt)

Verification report

The output resolves the task correctly. All requested limits exist, the stated formulas follow from the specified division rule, and the exact algorithm has polynomial bit complexity. No major or minor issues were found.

1. Finite-population weights

The local mass \(a_v=\sum_{t:h(t)=v}\mu_t\) correctly counts directly attached voters through \(Na_v\).

For every admissible \(N\), each supported type has a positive integer count: positivity of \(\mu_t\) and integrality of \(N\mu_t\) imply \(N\mu_t\geq1\). Consequently, connector-subtree activity is independent of \(N\).

At an active connector \(v\), the eligible children consist exactly of its \(Na_v\) voter leaves and its \(k_v\) active connector children. Thus the divisor \(Na_v+k_v\) is correct. Inactive connectors need no division in the argument.

For a supported type attached at \(v\), multiplying the division factors along the unique root-to-leaf path gives precisely the displayed formula for \(w_t^{(N)}\). It includes the final division at \(v\), and no additional division occurs at the voter leaf.

All denominators used are positive:

The assertion that all leaves of the same type receive the same weight is justified by their common parent and equal division.

2. Existence and identification of the limits

The factor \(N/(Na_v+k_v)\) converges to \(1/a_v\), since \(a_v>0\).

For every strict ancestor \(u\), the stated alternatives are exhaustive and correct. If \(a_u=0\), its factor is constantly \(1/k_u\); if \(a_u>0\), its factor converges to zero. There are finitely many factors, each with a finite limit, so taking their product is justified.

Therefore:

Multiplying by \(\mu_t\) gives the stated formulas for \(\alpha_t\). Since supported masses are strictly positive, the characterization of positive limiting weights is exact.

The product-of-denominators argument correctly establishes arbitrarily large admissible population sizes. It requires neither reduced input fractions nor a least common denominator.

The normalization argument is also valid. The finite identity sums the weights of all voter leaves, and passage to the limit is justified because the support size \(\tau\) is fixed and finite.

3. Algorithm correctness

The common-denominator construction is exact: each \(D/d_t\) is an integer, \(b_t=D\mu_t\), and \(B_v=Da_v\).

The bottom-up activity recurrence matches the definition of an active connector subtree and computes every \(k_v\).

The top-down recurrence \(P_c=P_vk_v\) correctly maintains the product over strict ancestors. For each traversed edge to an active child, \(k_v\geq1\), so this recurrence never introduces a zero factor.

The Boolean update correctly records whether a strict ancestor has positive local mass. At a supported attachment vertex, the Boolean is false exactly when that vertex belongs to \(F\). Substituting \(a_v=B_v/D\) into the proved formulas gives exactly the algorithm’s output fractions.

No expanded population network is needed.

4. Running time and bit complexity

The claimed operation count is justified: grouping types, rooting and traversing the tree, forming the integer masses, and producing the outputs require \(O(m+\tau)\) graph and arithmetic operations.

The integer-size bounds are correct:

Products used in output denominators therefore also have \(O(L+m)\) bits. Schoolbook arithmetic supports the stated conservative bound \(O(L+(m+\tau)(L+m)^2)\). Optional fraction reduction by quadratic-time gcd computation fits within that bound.

For the explicitly stated standard tree encoding, \(m=O(L)\), giving \(O((m+\tau)L^2)\) bit operations. The output-length bound \(O(\tau(L+m))\) is consistent with the numerator and denominator sizes.

5. Edge cases and citation

The argument covers \(m=1\), attachments at the root, multiple types sharing a connector, inactive branches, and occupied vertices below other occupied vertices. Empty ancestor products and the root Boolean are handled explicitly.

The cited Theorem 6 does state that finite-network LEGIT+ weights are computable in \(O(|V|+|E|)\) time. Its network assumptions hold for the expanded trees here. The prover uses this citation only for context; the continuous-limit result is established independently. [Brill, Conitzer, Freeman, and Shah, Theorem 6](https://www.cs.cmu.edu/~conitzer/FNPrecAAMAS16full.pdf).

Repair feedback: None required.

⟨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.