Answer: Polynomial-time solvable in \(m,\tau,L,p\), uniformly over all four semantics.
Lemma 1 — class: algorithmic
PDF text-layer excerpt — equations and symbol order may be approximateIf a semantics σ satisfies Bi-variate Equivalence, Bi- variate Proportionality, and Bi-variate Reinforcement then the lower bound (resp. the upper bound) of the final acceptability interval can be computed by using the case where the initial weight is the lowest (resp. the highest), the attackers are at their strongest (resp. weakest), and the supporters are at their weakest (resp. strongest). Note that in that case the complexity of computing final inter- vals remains the same as the complexity of computing the seman- tics itself. This applies to QuAD, DF-QuAD, Exb, and QuEM, since they satisfy these principles.
statement extracted from the paper’s text layer; consult the paper for the exact wording
Given an acyclic debate graph, a semantics \(\sigma\), a finite set of complete response types \(T\), a rational distribution \(\mu\) over \(T\), a population scale \(N\), and an IDM parameter \(\beta\), compute the final acceptability interval for every claim. Each type records, for every claim, abstention or a score in \(\{0,1,2,3,4\}\); use vote masses \(k_{a,l}=N\sum_{t:t(a)=l}\mu_t\) to form the paper's normalized IDM initial intervals, then propagate their bounds using \(\sigma\).
Let \(A\) be a set of \(m\geq1\) claims, with disjoint attack and support relations \(R^-,R^+\subseteq A\times A\) whose union is acyclic; write \(R^\pm(a)=\{b:(b,a)\in R^\pm\}\).
A society is given by its support: a list of \(\tau\) distinct types \(t:A\to\{\bot,0,1,2,3,4\}\), each with positive binary-rational mass \(\mu_t\), with \(\sum_t\mu_t=1\); \(\bot\) means abstention. Here \(\tau\) is the support size, not the number of possible types. The population scale \(N>0\) and IDM parameter \(\beta>0\) are binary rationals; \(L\) is the total binary input length excluding the precision parameter.
Set \(k_{a,l}=N\sum_{t:t(a)=l}\mu_t\), \(K_a=\sum_{l=0}^4k_{a,l}\), \(S_a=\sum_{l=0}^4l k_{a,l}\), and the normalized initial interval \(I_a=[S_a/(4(K_a+\beta)),(S_a+4\beta)/(4(K_a+\beta))]\).
The input selects \(\sigma\in\{\mathrm{QuAD},\mathrm{DF\text{-}QuAD},\mathrm{Exb},\mathrm{QuEM}\}\). For initial weight \(x\in[0,1]\), attacker vector \(y\), and supporter vector \(z\), put \(P_- =\prod_i(1-y_i)\), \(P_+=\prod_j(1-z_j)\), \(d=P_--P_+\), and \(e=\sum_jz_j-\sum_i y_i\); empty products equal \(1\).
For QuAD, put \(f_-=xP_-\), \(f_+=1-(1-x)P_+\): the value is \(x\) if both vectors contain only zeros, \(f_-\) if only the supporter vector contains only zeros, \(f_+\) if only the attacker vector contains only zeros, and \((f_-+f_+)/2\) otherwise; an empty vector contains only zeros.
Define \(\sigma_{\mathrm{DF\text{-}QuAD}}=x+xd\) when \(d\leq0\), and \(x+(1-x)d\) otherwise; define \(\sigma_{\mathrm{Exb}}=1-(1-x^2)/(1+x2^e)\).
For \(h(v)=\max(v,0)^2/(1+\max(v,0)^2)\), define \(\sigma_{\mathrm{QuEM}}=x+(1-x)h(e)\) when \(e>0\), and \(x-xh(-e)\) otherwise.
Recursively define \(J_a=[\min\sigma(x,y,z),\max\sigma(x,y,z)]\), where \(x\in I_a\), \(y_b\in J_b\) for each \(b\in R^-(a)\), and \(z_c\in J_c\) for each \(c\in R^+(a)\). These choices vary independently, including when predecessors share ancestors.
The computational problem is to evaluate every endpoint of every \(J_a\) to absolute error at most \(2^{-p}\), for a supplied positive integer precision \(p\), in the binary Turing model.
Is this endpoint-computation problem solvable in time polynomial in \(m,\tau,L,p\), uniformly over the four choices of \(\sigma\), or is it NP-hard?
For finite integer populations, endpoint selection is known to preserve the evaluation complexity of these semantics, giving polynomial-time interval computation on acyclic graphs; this result also permits arbitrary supplied initial intervals. [Source](https://journals.sagepub.com/doi/10.3233/FAIA250995)
No verified result located establishes the binary running-time bound for the mass-input and precision formulation above.
The endpoint-computation problem is solvable in deterministic time polynomial in \(m,\tau,L,p\), uniformly over the four specified semantics.
The proof requires both endpoint selection and a binary precision analysis. QuAD needs special treatment because it is discontinuous when an attacker or supporter vector changes from all zeros to containing a positive entry. Exact Boolean flags suffice to handle those discontinuities.
The cited paper states the endpoint-selection principle in Lemma 1. [Uncertainty in Quantitative Bipolar Argumentation Frameworks](https://journals.sagepub.com/doi/10.3233/FAIA250995). We prove that principle directly for the formulas in the question, and then establish the required binary running-time bound.
Write \(I_a=[i_a^-,i_a^+]\) and \(J_a=[j_a^-,j_a^+]\).
Because \(0\leq S_a\leq4K_a\) and \(\beta>0\), the supplied formula gives \(0\leq i_a^-\leq i_a^+\leq1\). The quantities \(K_a,S_a,i_a^-,i_a^+\) can be computed exactly by rational arithmetic in polynomial time: each sum has at most \(\tau\) terms, and common denominators can be formed by multiplying input denominators, whose total binary length is polynomial in \(L\). Thus their exact rational representations have polynomial length.
We next prove that every semantics is nondecreasing in \(x\) and every supporter coordinate, and nonincreasing in every attacker coordinate.
For all inputs in the unit cube,
\(f_-=xP_-\leq x\leq1-(1-x)P_+=f_+\).
Within each fixed branch, the required monotonicities follow directly from the product formulas.
The only possible branch change when an attacker coordinate increases occurs when that coordinate changes from zero to positive and all other attackers are zero. If supporters are all zero, the formula remains \(xP_-\). Otherwise, the value changes from \(f_+\) to \((f_-+f_+)/2\), which is at most \(f_+\). Subsequent increases decrease \(f_-\). Hence increasing an attacker never increases the output.
Similarly, when the first positive supporter appears while attackers are nonzero, the value changes from \(f_-\) to \((f_-+f_+)/2\), which is at least \(f_-\). If attackers are all zero, the formula remains \(f_+\). Hence increasing a supporter never decreases the output.
The branch depends only on the predecessor vectors, and every branch is nondecreasing in \(x\).
Write its value as \(F(x,d)\). Since \(P_-,P_+\in[0,1]\), we have \(d\in[-1,1]\). Its branches are
\(F(x,d)=x(1+d)\) for \(d\leq0\), and \(F(x,d)=d+(1-d)x\) for \(d\geq0\).
Both are nondecreasing in \(x\) and \(d\), and agree at \(d=0\). Increasing an attacker decreases \(d\); increasing a supporter increases \(d\).
Put \(T=2^e>0\). Then
\(F(x,e)=\dfrac{xT+x^2}{1+xT}\).
Direct differentiation gives
\(\dfrac{\partial F}{\partial x}=\dfrac{T+2x+x^2T}{(1+xT)^2}\geq0\),
and
\(\dfrac{\partial F}{\partial e}=(\ln2)\dfrac{xT(1-x^2)}{(1+xT)^2}\geq0\).
Since increasing an attacker decreases \(e\), and increasing a supporter increases \(e\), the required monotonicities follow.
The definition simplifies to
\(F(x,e)=\dfrac{x}{1+e^2}\) for \(e\leq0\), and \(F(x,e)=\dfrac{x+e^2}{1+e^2}\) for \(e\geq0\).
The branches agree at \(e=0\). Each is nondecreasing in \(x\). Their derivatives with respect to \(e\) are respectively
\(\dfrac{-2ex}{(1+e^2)^2}\geq0\) and \(\dfrac{2e(1-x)}{(1+e^2)^2}\geq0\).
Thus the required monotonicities again hold.
All four semantics take values in \([0,1]\): QuAD uses values or averages between \(f_-\) and \(f_+\); DF-QuAD uses the displayed branches with \(d\in[-1,1]\); and the displayed Exb and QuEM fractions lie in \([0,1]\).
Coordinatewise monotonicity gives the exact identities
\(j_a^-=\sigma\bigl(i_a^-,(j_b^+)_{b\in R^-(a)},(j_c^-)_{c\in R^+(a)}\bigr)\),
\(j_a^+=\sigma\bigl(i_a^+,(j_b^-)_{b\in R^-(a)},(j_c^+)_{c\in R^+(a)}\bigr)\).
Indeed, replacing each coordinate by its indicated extremal value can only decrease, respectively increase, the output. These corners belong to the admissible box, so the extrema are attained. Continuity is unnecessary.
This argument uses the stipulated independence of predecessor choices, including choices for predecessors with shared ancestors. A topological order therefore reduces the problem to two local evaluations per claim.
Rounded numerical values alone cannot safely determine whether a true predecessor value is zero. We instead maintain two exact flags for every endpoint \(v\):
\(Z(v)\) means \(v=0\), and \(O(v)\) means \(v=1\).
For initial endpoints, these flags are obtained by exact rational comparisons.
For a QuAD evaluation, define:
Universal assertions about empty vectors are true; existential assertions are false.
If \(v=\sigma_{\mathrm{QuAD}}(x,y,z)\), then
\(Z(v)=Z_+\land\bigl(Z(x)\lor O_-\bigr)\),
\(O(v)=Z_-\land\bigl(O(x)\lor O_+\bigr)\).
To prove the first identity, if supporters are all zero, every applicable branch equals \(xP_-\). This is zero exactly when \(x=0\) or some attacker equals one. If a supporter is positive, then \(P_+<1\), so \(f_+>0\); the selected branch is either \(f_+\) or an average containing \(f_+\), and is positive.
For the second identity, if attackers are all zero, every applicable branch equals \(f_+\). This equals one exactly when \(x=1\) or some supporter equals one. If an attacker is positive, then \(P_-<1\), so \(f_-<1\); the selected branch is either \(f_-\) or an average containing \(f_-\), and is strictly below one.
Consequently, all flags and all QuAD branch choices can be propagated exactly in topological order using polynomially many Boolean operations. The numerical computation uses the branch selected by these exact flags, even if rounding makes a positive predecessor appear zero.
For a tuple \(w=(x,y,z)\), let \(\|w-w'\|_1\) denote the sum of the absolute coordinate differences. Set
\(B=2^{m+2}\).
We will use the bound
\(\lvert F(w)-F(w')\rvert\leq B\|w-w'\|_1\).
For the three continuous semantics, this holds globally on the relevant input cube. For QuAD, it holds for each fixed branch expression, considered as a function on the whole cube. That is sufficient because the branch is selected exactly.
For factors in \([0,1]\), telescoping the products proves
\(\left|\prod_i u_i-\prod_i v_i\right|\leq\sum_i|u_i-v_i|\).
It follows that \(x\), \(f_-\), \(f_+\), and \((f_-+f_+)/2\) each satisfy the stronger bound with coefficient \(1\).
For fixed \(d\), the slopes in \(x\) are \(1+d\) or \(1-d\), both in \([0,1]\). For fixed \(x\), the slopes in \(d\) are \(x\) or \(1-x\), also in \([0,1]\). Agreement at \(d=0\) therefore gives
\(|F(x,d)-F(x',d')|\leq|x-x'|+|d-d'|\).
The product inequality gives
\(|d-d'|\leq\sum_i|y_i-y_i'|+\sum_j|z_j-z_j'|\).
For \(v\geq0\),
\(h'(v)=\dfrac{2v}{(1+v^2)^2}\leq1\),
because \(2v\leq1+v^2\). Thus the absolute slopes in \(x\) and \(e\) are at most one. The branches agree at zero, so
\(|F(x,e)-F(x',e')|\leq|x-x'|+|e-e'|\).
Also,
\(|e-e'|\leq\sum_i|y_i-y_i'|+\sum_j|z_j-z_j'|\).
There are at most \(m-1\) predecessors, so \(|e|\leq m\) and \(T\leq2^m\). The derivatives already computed satisfy
\(0\leq\dfrac{\partial F}{\partial x}\leq2T+2\leq2^{m+2}=B\).
Writing \(r=xT\geq0\), we also obtain
\(0\leq\dfrac{\partial F}{\partial e}\leq(\ln2)\dfrac{r}{(1+r)^2}\leq\dfrac{\ln2}{4}<1\),
where \(4r\leq(1+r)^2\). This proves the asserted bound.
The factor \(B\) is exponential in \(m\), but its binary logarithm is linear in \(m\). Hence it requires only polynomially many guard bits.
Fix an integer working precision \(q\geq1\), and put \(\delta=2^{-q}\). Store numerical endpoint approximations as dyadic rationals on the grid with spacing \(\delta\), rounded to \([0,1]\).
We show that a local evaluation on these rounded inputs can be computed with absolute error at most \(\delta\) in time polynomial in \(m,q\).
For QuAD with its branch fixed, DF-QuAD, and QuEM, evaluate the selected formula exactly on the dyadic inputs, then round to the grid. Each product has at most \(m-1\) factors, so its binary length is \(O(mq)\). The sums, squares, comparisons, and divisions also involve polynomial-length rationals. Thus exact local evaluation and rounding take polynomial time.
For DF-QuAD and QuEM, branch comparisons are made on the rounded inputs. Their global sensitivity bounds already account for any difference from the branch at the true inputs.
For completeness, we give an explicit rational approximation procedure for Exb.
Here \(e\) is the exact signed sum of the rounded predecessor values, and \(|e|\leq m\).
Use
\(\ln2=2\sum_{k=0}^{\infty}\dfrac{1}{(2k+1)3^{2k+1}}\).
This identity follows by integrating the geometric series for \(1/(1-v^2)\) from zero to \(1/3\). Its convergence is uniform on that interval, which justifies termwise integration.
Let \(\ell\) be the sum of its first \(n=q+3m+6\) terms. Then
\(0<\ell<\ln2<1\),
and the tail satisfies
\(|\ell-\ln2|\leq\dfrac34\,9^{-n}\leq2^{-n}\).
Put \(u=e\ell\). By the mean-value theorem,
\(|\exp(u)-2^e|\leq\exp(m)\,m\,2^{-n}\).
Since \(\exp(1)<4\), we have \(\exp(m)\leq2^{2m}\). Also \(m2^{-m}\leq1\). Consequently,
\(|\exp(u)-2^e|\leq2^{-q-6}\).
Now choose
\(s=\max\{2m^2,q+2m+6\}\), and \(r=2s\),
and compute the rational Taylor sum
\(T_0=\sum_{j=0}^{r-1}\dfrac{u^j}{j!}\).
Taylor's theorem and \(|u|\leq m\) give
\(|\exp(u)-T_0|\leq\exp(m)\dfrac{m^{2s}}{(2s)!}\).
The last \(s\) factors of \((2s)!\) are each at least \(s\), so \((2s)!\geq s^s\). Therefore,
\(|\exp(u)-T_0|\leq2^{2m}\left(\dfrac{m^2}{s}\right)^s\leq2^{2m-s}\leq2^{-q-6}\).
Set \(\widetilde T=\max(T_0,0)\). Projection onto the nonnegative half-line cannot increase the error relative to \(2^e>0\), so
\(|\widetilde T-2^e|\leq2^{-q-5}\).
Both finite sums use polynomially many terms. Every term and intermediate rational has polynomial binary length: the logarithm sum has polynomial-length common denominators, and the Taylor sum uses powers of a polynomial-length rational and factorials of polynomially bounded integers. Exact computation of these sums is therefore polynomial in \(m,q\).
For fixed \(x\in[0,1]\), define
\(G(x,T)=1-\dfrac{1-x^2}{1+xT}\).
For \(T\geq0\),
\(\left|\dfrac{\partial G}{\partial T}\right|=\dfrac{x(1-x^2)}{(1+xT)^2}\leq1\).
Thus substituting \(\widetilde T\) incurs error at most \(\delta/32\). Evaluating the resulting rational exactly and rounding to the nearest dyadic grid point incurs another error at most \(\delta/2\). The total local error is strictly below \(\delta\), as required.
Let
\(H=m+2+\lceil\log_2m\rceil\), and \(D=mB\leq2^H\).
Choose
\(q=p+mH+2\), so \(\delta=2^{-q}\).
First round every initial endpoint with error at most \(\delta\). Then process claims in topological order, using the corner formulas from Section 2. For QuAD, propagate exact flags and evaluate the branch selected by them. For every semantics, use the local procedures from Section 5.
Let \(E_r\) be the maximum of \(\delta\) and the absolute errors in all endpoints computed for the first \(r\) claims. Put \(E_0=\delta\).
At the next claim, its initial endpoint has error at most \(\delta\leq E_{r-1}\), and every selected predecessor endpoint has error at most \(E_{r-1}\). There are at most \(m\) input coordinates, including the initial endpoint. The sensitivity bound therefore gives an error at most \(D E_{r-1}\) before local numerical evaluation.
For QuAD, this comparison uses the same exact branch expression at the true and rounded tuples, as ensured by the flags. Thus its discontinuities do not invalidate the estimate.
Adding local evaluation error yields
\(E_r\leq\delta+D E_{r-1}\).
Induction gives
\(E_r\leq\delta\sum_{j=0}^{r}D^j\leq2\delta D^r\),
where the last inequality uses \(D\geq2\). Hence
\(E_m\leq2\,2^{-q}2^{mH}=2^{-p-1}\leq2^{-p}\).
This bounds every output endpoint.
Finally,
\(q=p+O(m^2+m\log m)\).
Initial rational arithmetic is polynomial in \(m,\tau,L\). There are exactly two local endpoint evaluations per claim, each polynomial in \(m,q\), and QuAD's flags require only polynomially many Boolean operations. The output itself has \(O(mq)\) bits.
Therefore the entire algorithm runs in time polynomial in \(m,\tau,L,p\), uniformly over the four semantics. The proof also applies to arbitrary supplied binary-rational initial intervals in \([0,1]\).
⟨structured verdict parsed — rendered above⟩
The prover’s claimed polynomial-time result is established. I found no mathematical errors, major gaps, or minor issues requiring clarification. The argument addresses the binary mass-input model and the requested absolute precision, including QuAD’s discontinuities.
The bounds \(0\leq S_a\leq4K_a\) and \(\beta>0\) imply that both initial endpoints are well-defined and lie in \([0,1]\). This includes \(K_a=0\), where the interval is \([0,1]\).
The exact arithmetic claim is valid. Summing the listed rational masses, multiplying by \(N\), and forming the endpoint fractions require only polynomial-length integers. Multiplying denominators adds their binary lengths; it does not create exponentially many bits. The construction uses the supplied \(\tau\) types and never enumerates all possible types.
All four monotonicity arguments check out.
The range assertions are also correct: every local evaluation remains in \([0,1]\).
The two corner identities follow from the established coordinatewise monotonicity. Each selected corner belongs to the admissible product of intervals, so the minimum and maximum are attained even for discontinuous QuAD.
The proof explicitly uses the independence required by the task. Shared ancestors therefore impose no additional constraint on the local choices.
Acyclicity of the union supplies a topological order. Disjointness and acyclicity also justify the later bound of at most \(m-1\) predecessor coordinates per claim.
The attribution to Lemma 1 is accurate: the cited paper states the same endpoint-selection principle. The prover independently establishes the needed property for the task’s formulas, so the proof does not depend on an unverified application of that lemma. [Source](https://journals.sagepub.com/doi/10.3233/FAIA250995)
Both Boolean identities are correct:
\[
Z(v)=Z_+\land\bigl(Z(x)\lor O_-\bigr),\qquad
O(v)=Z_-\land\bigl(O(x)\lor O_+\bigr).
\]
If supporters are all zero, the output equals \(xP_-\), with precisely the stated zero conditions. If some supporter is positive, \(f_+>0\), and every applicable output is positive.
Dually, if attackers are all zero, the output equals \(f_+\), with precisely the stated conditions for equality to one. If some attacker is positive, \(f_-<1\), and every applicable output is strictly below one.
The empty-vector conventions are consistent with these identities. Exact initial flags and topological propagation suffice to select every true QuAD branch without testing rounded numerical values.
The product inequality is valid for factors in \([0,1]\). It yields the stated coefficient-one bounds for each fixed QuAD expression and for the product contribution to DF-QuAD.
The DF-QuAD slopes have absolute value at most one. The QuEM estimate \(h'(v)\leq1\) is valid, and agreement at zero permits the claimed global bound across its branches.
For Exb, \(|e|\leq m\) gives \(T\leq2^m\). The bounds
\[
\frac{\partial F}{\partial x}\leq2T+2\leq2^{m+2},
\qquad
\frac{\partial F}{\partial e}\leq\frac{\ln2}{4}<1
\]
are correct. Thus \(B=2^{m+2}\) is a valid common sensitivity coefficient.
QuAD is appropriately treated using the fixed expression selected by exact flags. The argument does not incorrectly assert global continuity or global Lipschitz continuity for QuAD itself.
For QuAD, DF-QuAD, and QuEM, exact evaluation on dyadic inputs uses polynomial-length rational arithmetic. Comparisons for the continuous piecewise semantics may safely use rounded inputs because their global sensitivity bounds cover branch changes.
The explicit Exb procedure also checks out:
Both finite sums have polynomially many terms and polynomial-length rational intermediates. No unit-cost assumption for transcendental evaluation is hidden in this procedure.
Each local tuple has at most \(m\) coordinates including \(x\). Consequently, the sensitivity estimate gives \(DE_{r-1}\), where \(D=mB\), and local evaluation adds at most \(\delta\).
The recurrence and geometric bound are valid:
\[
E_r\leq\delta+DE_{r-1}
\leq\delta\sum_{j=0}^{r}D^j
\leq2\delta D^r.
\]
The maximum with \(\delta\) in the definition of \(E_r\) causes no problem: the proposed recurrence bound also dominates all previously computed errors.
With \(q=p+mH+2\) and \(D\leq2^H\), the final bound is indeed
\[
E_m\leq2^{-p-1}\leq2^{-p}.
\]
This includes \(m=1\) and claims with no predecessors. The working precision is polynomial in \(m,p\); initialization is polynomial in \(m,\tau,L\); and the number and cost of local evaluations are polynomial. The extension to supplied binary-rational initial intervals in \([0,1]\) is supported by the same argument.
No repair or additional clarification is needed.
⟨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.