Answer: Polynomial-time solvable
Proposition 20 — class: other
PDF text-layer excerpt — equations and symbol order may be approximateLet $\mca$ and $S$ be as in Definition~\ref{def-fusion}, $\sqsupseteq_S$, a total pre-order, and $A = \fuse(\mca)$.
statement extracted from the paper’s text layer; consult the paper for the exact wording
Given a finite set of worlds \(\Omega\), finite ordered credibility ranks \(R\), and a distribution \(\mu\) with binary rational masses over \(\tau\) explicitly represented pedigreed agent types \(t=(\prec^t,\ell^t)\), compute the fused pedigreed state and its induced belief state. Put \((x,y)\) in the fused relation \(\prec\) if some \(t\in\operatorname{supp}(\mu)\) and \(r\in R\) have \((x,y)\in\prec^t_r\), and every supported type \(u\) is agnostic in both directions at every rank \(r'>r\). Set \(\ell(x,y)=\max\{r:(x,y)\in\prec^t_r\text{ for some }t\in\operatorname{supp}(\mu)\}\); return \((\prec,\ell)\) and the induced relation \(\prec^+\).
Let \(\Omega\) be a nonempty finite set of worlds, \(m=|\Omega|\), and \(R\) a nonempty finite totally ordered set of credibility ranks; larger ranks mean greater credibility.
A society is given by its support: the list \(T\) of its \(\tau\) types with positive binary rational masses \(\mu(t)\), summing to \(1\). Here \(\tau\) is the support size, not the number of possible types. Let \(L\) be the total binary input length.
Each type is an explicitly represented pair \(t=(\prec^t,\ell^t)\), with \(\prec^t\subseteq\Omega^2\) and \(\ell^t:\prec^t\to R\). Validity is promised: it arises from a finite family of source relations \(Q_s\), each transitive and modular, with ranks \(\rho_s\in R\). Modularity means \(xQ_sy\Rightarrow(xQ_sz\lor zQ_sy)\) for all worlds.
Precisely, \(x\prec^t y\) iff some source \(s\) has \(xQ_sy\) and every source \(v\) with \(\rho_v>\rho_s\) has neither \(xQ_vy\) nor \(yQ_vx\); on retained pairs, \(\ell^t(x,y)=\max\{\rho_s:xQ_sy\}\). These source families are not supplied. Empty families, conflicts, and diagonal pairs are allowed.
Write \(\prec^t_r=\{(x,y)\in\prec^t:\ell^t(x,y)=r\}\); agnosticism at rank \(r\) means that neither direction belongs to \(\prec^t_r\).
The required fused relation contains \((x,y)\) iff some \(t\in T\) and \(r\in R\) satisfy \((x,y)\in\prec^t_r\), while every \(u\in T\) is agnostic on this pair at every \(r'>r\). Define \(\ell:\prec\to R\) by \(\ell(x,y)=\max\{r:\exists t\in T,\ (x,y)\in\prec^t_r\}\). Return explicitly \((\prec,\ell)\) and its induced belief state \(\prec^+\), the transitive closure using paths of positive length.
Can this fusion computation be performed in polynomial time in \(m,\tau,|R|,L\), or is it NP-hard?
For finite agent sets, labeled refinement reconstructs the pedigreed state of the union of their informant sources; its transitive closure is the induced belief state. [Discrete reconstruction result](https://arxiv.org/pdf/cs/0203013)
The later journal treatment retains this reconstruction result. No result explicitly treating the binary rational support-distribution formulation was located. [Journal treatment](https://www.cs.cmu.edu/afs/cs/project/jair/pub/volume19/maynard03a.pdf)
The fusion computation is polynomial-time solvable in \(m,\tau,|R|,L\). The binary rational masses affect neither the fused relation nor its labels: the stated rule depends only on which types belong to the positive support.
The proof below gives an explicit algorithm, including the positive-length transitive closure. It applies even without the validity promise, so recovering the hidden source families is unnecessary.
Introduce a sentinel \(\bot\notin R\), ordered below every rank. For each ordered pair \((x,y)\in\Omega^2\), define
\[
a(x,y)=\max\bigl(\{\ell^t(x,y):t\in T,\ (x,y)\in\prec^t\}\cup\{\bot\}\bigr).
\]
Here and below, this formula is written equivalently in inline notation as \(a(x,y)=\max(\{\ell^t(x,y):t\in T,\ (x,y)\in\prec^t\}\cup\{\bot\})\).
Define the greatest rank at which either direction is represented by
\(h(x,y)=\max\{a(x,y),a(y,x)\}\).
Lemma. For every \(x,y\in\Omega\),
\((x,y)\in\prec\) if and only if \(a(x,y)=h(x,y)\ne\bot\).
Whenever this holds, \(\ell(x,y)=h(x,y)\).
Proof. Suppose first that \((x,y)\in\prec\). By the fusion definition, some type \(t\) supports \((x,y)\) at a rank \(r\), and every type is agnostic on this pair at every rank strictly above \(r\).
The witness gives \(a(x,y)\ge r\). The agnosticism condition says that neither direction occurs in any type at a rank above \(r\). Consequently, \(a(x,y)\le r\) and \(a(y,x)\le r\). Thus \(a(x,y)=h(x,y)=r\ne\bot\).
Conversely, suppose \(a(x,y)=h(x,y)\ne\bot\), and put \(r=h(x,y)\). The maximum defining \(a(x,y)\) is attained because the support is finite. Hence some type supports \((x,y)\) at rank \(r\). Since both directional maxima are at most \(r\), no type supports either direction at any rank above \(r\). Every type is therefore agnostic at those higher ranks, as required.
Finally, the label prescribed in the question is exactly the maximum defining \(a(x,y)\). On a retained pair this equals \(h(x,y)\). This proves the lemma. \(\square\)
This characterization handles ties explicitly: if both directions attain the greatest represented rank, both survive.
Represent the ranks by their positions in the given total order, using the integer \(0\) for \(\bot\).
After the scan, \(A\) represents \(a\). The lemma therefore proves that step 3 outputs exactly \((\prec,\ell)\).
All masses are positive, so the supplied list already identifies the relevant support. No rational arithmetic or expansion into a population of agents is needed.
Regard \(\prec\) as the edge relation of a directed graph on \(\Omega\). For each starting world \(x\), perform a graph search as follows:
Soundness. Every initially visited vertex is reached from \(x\) by one edge. Every subsequent addition extends an already established positive-length path by one edge. Thus every reported pair belongs to \(\prec^+\).
Completeness. Let \(x=v_0,v_1,\ldots,v_q=y\) be a path with \(q\ge1\). The initialization visits \(v_1\). Inductively, once \(v_i\) is visited, it is eventually processed, and its successor \(v_{i+1}\) is visited. Hence \(y\) is visited.
In particular, the algorithm does not insert a diagonal pair merely because a vertex reaches itself by a path of length zero. It reports \((x,x)\) exactly when there is a positive-length return path, including a supplied self-loop.
Put \(k=|R|\), and let \(E\) be the total number of labeled pair occurrences across all support types. Since each type contains at most \(m^2\) ordered pairs, \(E\le\tau m^2\).
Once worlds and ranks are indexed:
Thus the main computation takes \(O(\tau m^2+m^3)\) elementary operations.
Input decoding and conversion of explicit world and rank identifiers to indices are polynomial in \(L,m,k\). Rank indices use \(O(\log(k+1))\) bits; vertex indices use \(O(\log(m+1))\) bits. Consequently, implementing the operations with their actual binary encodings gives a polynomial bit-time bound in \(m,\tau,k,L\).
Each returned relation has at most \(m^2\) pairs. Output labels can reference the input ranks, so explicit output also has polynomial length.
The finite-agent reconstruction statement appears as Proposition 20 in the [discrete treatment](https://arxiv.org/pdf/cs/0203013) and as Definition 23 and Proposition 22 in the [journal treatment](https://www.cs.cmu.edu/afs/cs/project/jair/pub/volume19/maynard03a.pdf).
The distribution formulation requires no additional reconstruction step. Its fusion definition quantifies over the explicitly listed support types, and numerical masses never enter that definition. The pairwise lemma and graph-search proof therefore establish the requested polynomial-time computation directly.
⟨structured verdict parsed — rendered above⟩
Assessment: proved. The output resolves the assigned computation problem with a correct explicit algorithm and a polynomial bit-time justification. No major or minor mathematical issues were found.
The prover correctly treats \(T\) as the explicitly listed positive support, rather than as the set of all possible types or an expanded population.
The fusion definition contains no numerical use of \(\mu(t)\). Consequently, ignoring the mass values after reading the input is justified. Their binary representation does not create a hidden enumeration requirement.
The claim that the algorithm does not require the validity promise is also correct: its proof uses only the supplied labeled relations and the stated fusion rule. It does not attempt to reconstruct or validate the hidden source families.
The definition of \(a(x,y)\) is well-defined. Every supplied label belongs to the finite totally ordered set \(R\), and adding \(\bot\) makes the set over which the maximum is taken nonempty. The quantity \(h(x,y)\) therefore exists for every ordered pair.
The forward implication is correct:
The reverse implication is also correct:
The label conclusion is justified independently of the membership argument: the prescribed label is precisely the directional maximum \(a(x,y)\), which equals \(h(x,y)\) on retained pairs.
Equal-rank conflicts are handled correctly. If both directions attain the greatest represented rank, both satisfy the membership condition and survive.
The table initialization represents the sentinel correctly. Each update takes a directional maximum, so after the scan the table contains exactly the indexed values of \(a\).
The final selection condition is precisely the proved characterization. Translating the selected index back to its input rank gives the required label.
No assumption of transitivity, modularity, asymmetry, or irreflexivity enters this computation. In particular, for a diagonal pair, the two directional table entries coincide; the algorithm retains that pair exactly when some type supplies it.
The search algorithm correctly distinguishes positive-length reachability from reflexive reachability.
Its soundness proof supplies a valid invariant: every visited vertex has a positive-length path from the starting world. Initialization establishes this using direct edges, and subsequent additions preserve it by extending a path.
Its completeness proof is valid. Every visited vertex is eventually processed because vertices are queued when first visited, each is queued at most once, and the graph is finite. Induction along any positive-length path therefore reaches its endpoint.
The stated treatment of diagonal pairs is correct:
Empty relations and a single-world domain are covered by the same argument.
The bound \(E\le\tau m^2\) follows from each type relation being a subset of \(\Omega^2\).
The initialization, scan, and selection costs are correct once identifiers are indexed. The search bound \(O(m(m+e))\), with \(e\le m^2\), gives \(O(m^3)\). Direct-successor lists can be produced during the existing output scan; this requires no larger asymptotic bound.
The distinction between elementary operations and bit operations is adequately addressed. Rank and vertex indices have logarithmic bit length, while decoding and indexing explicit identifiers require polynomial time in the supplied input length and parameters. Reading binary rational masses also fits within input decoding; no arithmetic with their values is required.
Both returned relations have at most \(m^2\) pairs, and their labels reference supplied ranks. The explicit-output requirement therefore introduces no superpolynomial output size.
The polynomial-time conclusion is established. As usual, this does not assert an unconditional separation from NP-hardness; the explicit polynomial-time algorithm answers the task’s computational question.
The cited locations are accurate: Proposition 20 in the [discrete treatment](https://arxiv.org/pdf/cs/0203013) gives labeled reconstruction, and Definition 23 with Proposition 22 in the [journal treatment](https://www.cs.cmu.edu/afs/cs/project/jair/pub/volume19/maynard03a.pdf) defines pedigreed fusion and identifies its result with the fused agent’s pedigreed state.
These citations provide context rather than premises of the algorithmic proof. The prover does not apply their reconstruction conclusions to arbitrary unpromised relations, and its polynomial-time result stands independently of them.
No mathematical repair or additional clarification is required. The pairwise lemma, closure argument, complexity analysis, and representation discussion together settle the assigned task.
⟨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.