Answer: The threshold decision problem is in \(\mathrm{P}\), and exact computation of \(M_\mu(\alpha,\beta)\) is in \(\mathrm{FP}\).
Theorem 2 — class: algorithmic
PDF text-layer excerpt — equations and symbol order may be approximateLet P be a monotonic Next-Variable Predicate, and let α, β ∈V be outcomes. The above procedure for lexicographic infer- ence is correct, i.e., it returns true if P |=lex α ≥β and it returns false otherwise. Decisive Sequence: A Lexicographic model (Y1, ≥1), . . . , (Yk, ≥k) is said to be a decisive sequence with respect to P and α ≥β if α(Yk) ̸≥k β(Yk), and for j = 1, . . . , k−1, α(Yj) = β(Yj), and, for j = 1, . . . , k, P(Aj, Yj, ≥j) holds, where Aj = {Y1, . . . , Yj−1}. Thus, if π is a decisive sequence with respect to P and α ≥β, then π satisfies P but not α ≥β.
statement extracted from the paper’s text layer; consult the paper for the exact wording
Given a finite support of input types \(t\), rational masses \(\mu_t\) summing to \(1\), each type’s preference statements \(\Gamma_t\), and outcomes \(\alpha,\beta\), compute \(M_\mu(\alpha,\beta)=\sum_t \mu_t\,\mathbf{1}[\Gamma_t \models_{\mathrm{lex}} \alpha \ge \beta]\), or decide whether \(M_\mu(\alpha,\beta)\ge\rho\) for a rational threshold \(\rho\).
Let \(V\) be a set of \(m\ge 1\) variables, each with an explicitly listed finite nonempty domain \(D(X)\). Outcomes are complete assignments in \(\Omega=\prod_{X\in V}D(X)\).
A society is given by its support: a list of \(\tau\) types with positive binary rational masses \(\mu_t\) summing to \(1\). Here \(\tau\) is the support size, not the number of possible types. Type \(t\) carries an explicitly listed finite set \(\Gamma_t\) of preference statements.
A statement \(p\ge q\parallel T\) has partial assignments \(p\) on \(P\subseteq V\) and \(q\) on \(Q\subseteq V\), with \(T\subseteq V\) and \((P\cup Q)\cap T=\varnothing\). It requires \(a\succeq b\) for every pair of outcomes extending \(p,q\), respectively, with \(a(T)=b(T)\); the three sets may be empty and \(P,Q\) may overlap.
A lexicographic model is a sequence of \(k\) distinct variables, \(1\le k\le m\), each equipped with a total order on its domain. It compares outcomes by the first selected variable on which they differ; outcomes agreeing on all selected variables are indifferent. Unselected variables are ignored.
Write \(\Gamma_t\models_{\mathrm{lex}}\alpha\ge\beta\) when every lexicographic model satisfying all statements in \(\Gamma_t\) ranks \(\alpha\) weakly above \(\beta\). If no such model exists, entailment holds vacuously.
Given outcomes \(\alpha,\beta\) and a binary rational threshold \(\rho\in[0,1]\), define \(M_\mu(\alpha,\beta)=\sum_t\mu_t\mathbf{1}[\Gamma_t\models_{\mathrm{lex}}\alpha\ge\beta]\). Let \(L\) be the total input bit length, \(d=\max_X|D(X)|\), and \(s=\sum_t|\Gamma_t|\); state running times in \(m,\tau,L,d,s\).
Is deciding whether \(M_\mu(\alpha,\beta)\ge\rho\) in polynomial time or NP-hard, and is exact computation of \(M_\mu(\alpha,\beta)\) possible in polynomial time?
Known discrete results: lexicographic entailment under monotonic next-variable predicates has a correct inference procedure; for the statement language above, entailment is computable in \(O(m^2|\Gamma|\bar d)\), where \(\bar d=m^{-1}\sum_X|D(X)|\). [Wilson (2014)](https://pdfs.semanticscholar.org/ea8e/b22b07ae169b0895e0f1bb0deb2333d62492.pdf)
Polynomial inference is also established for a richer language allowing strict and non-strict statements. [Wilson and George (2017)](https://www.ijcai.org/proceedings/2017/0182.pdf) No result for this exact rational-mass aggregation problem was located.
The threshold decision problem is in \(\mathrm{P}\), and exact computation of \(M_\mu(\alpha,\beta)\) is in \(\mathrm{FP}\).
The essential point is that the input explicitly lists the \(\tau\) supported types. We perform one polynomial-time entailment test per type and then add the selected rational masses exactly.
Use the given discrete entailment theorem: for this statement language, deciding \(\Gamma\models_{\mathrm{lex}}\alpha\ge\beta\) takes \(O(m^2|\Gamma|\bar d)\) elementary operations, where \(\bar d=m^{-1}\sum_{X\in V}|D(X)|\). The cited paper uses the same partial-assignment statement semantics and lexicographic models with distinct selected variables, total domain orders, and indifference when all selected values agree. Its universal definition of entailment also includes vacuous entailment for inconsistent premises. Thus the theorem applies to the present task. [Wilson (2014), Sections 2.1–2.2 and 4](https://pdfs.semanticscholar.org/ea8e/b22b07ae169b0895e0f1bb0deb2333d62492.pdf)
For each supported type, compute the bit \(e_t=\mathbf{1}[\Gamma_t\models_{\mathrm{lex}}\alpha\ge\beta]\).
Empty premise sets require a minor bookkeeping convention because the quoted running-time expression contains \(|\Gamma|\). If \(\Gamma_t=\varnothing\), then \(e_t=1\) precisely when \(\alpha=\beta\). Indeed, identical outcomes are indifferent in every model. Otherwise, choose a variable on which they differ and a one-variable model placing \(\beta\)'s value strictly above \(\alpha\)'s value. This model satisfies the empty premise set and refutes entailment.
Since \(\bar d\le d\), all entailment bits can therefore be computed in \(O(m^2d(s+\tau))\) elementary operations. This bound includes the empty-set cases and bookkeeping.
Write each input mass as \(\mu_t=a_t/b_t\), where \(a_t,b_t\) are positive binary integers. The fractions need not be reduced.
Define the positive common denominator \(Q=\prod_{t=1}^{\tau}b_t\), and the integer \(A=\sum_{t=1}^{\tau}e_ta_t(Q/b_t)\). Every division is exact because \(b_t\) divides \(Q\). Consequently,
\[ M_\mu(\alpha,\beta)=\frac{A}{Q}. \]
The large numerical value of \(Q\) does not cause an exponential output length. If \(\ell(n)\) denotes the binary length of a positive integer, then \(\ell(Q)\le 1+\sum_{t=1}^{\tau}\ell(b_t)=O(L)\).
Moreover, the promise that the masses sum to one gives \(\sum_{t=1}^{\tau}a_t(Q/b_t)=Q\). Since each \(e_t\) is either zero or one, it follows that \(0\le A\le Q\). Thus \(A\) also has \(O(L)\) bits, and the exact output fraction has polynomial length.
Using schoolbook integer arithmetic, forming \(Q\), computing the exact quotients, and accumulating \(A\) takes \(O(\tau L^2)\) bit operations. Every intermediate integer has \(O(L)\) bits. Returning \(A/Q\) is already an exact answer; reducing the fraction, if desired, also takes polynomial time.
Write the threshold as \(\rho=h/c\), with \(c>0\) and \(0\le h\le c\). Because both denominators are positive,
\[ M_\mu(\alpha,\beta)\ge\rho \quad\Longleftrightarrow\quad Ac\ge hQ. \]
Both products have \(O(L)\) bits, so this comparison takes \(O(L^2)\) bit operations. It preserves equality exactly and introduces no rounding error.
After polynomial-time indexing of the explicitly listed input, the entailment stage takes \(O(m^2d(s+\tau))\) elementary discrete operations, and rational aggregation takes \(O(\tau L^2)\) bit operations. Charging conservatively \(O(L)\) bit operations for each elementary discrete operation gives the overall bound
\[ O\!\left(m^2d(s+\tau)L+\tau L^2\right). \]
This bound covers both exact computation and threshold decision. Explicit listing ensures that \(m,\tau,d,s\) are bounded by the input length, so the bound is polynomial in \(L\).
Therefore the threshold problem is polynomial-time solvable; an NP-hardness result under polynomial-time reductions would imply \(\mathrm{P}=\mathrm{NP}\). Exact aggregation is likewise polynomial-time computable.
⟨structured verdict parsed — rendered above⟩
The prover resolves both parts of the task correctly. The threshold problem is in \(\mathrm{P}\), and exact computation is in \(\mathrm{FP}\). No major or minor mathematical issues were found.
The prover states the required theorem precisely: entailment for this statement language can be decided in \(O(m^2|\Gamma|\bar d)\) elementary operations.
The citation supports its application. Section 2.1 defines statements using arbitrary subsets \(P,Q,T\) satisfying \((P\cup Q)\cap T=\varnothing\), with exactly the outcome-pair semantics in the task. It imposes no additional disjointness condition on \(P,Q\); empty subsets are allowed. Section 2.2 uses distinct selected variables, total domain orders, and indifference when outcomes agree on every selected variable. Entailment universally quantifies over satisfying models, so inconsistent premises entail vacuously. Section 4.4 gives the claimed complexity bound. The paper’s consistency discussion also confirms that its intended model convention excludes empty sequences. Thus no hypothesis mismatch invalidates the theorem application. [Wilson (2014), Sections 2.1–2.2, 3.2, and 4.4](https://pdfs.semanticscholar.org/ea8e/b22b07ae169b0895e0f1bb0deb2333d62492.pdf)
The task explicitly supplies the discrete entailment result, so the prover need not reproduce its proof.
The stated characterization is correct. If \(\alpha=\beta\), every model ranks them indifferently. If they differ, the variable chosen by the prover has two distinct domain values, so a total order placing \(\beta\)'s value above \(\alpha\)'s exists. The resulting one-variable model is permitted because \(m\ge1\), and it satisfies the empty premise set.
This handles the zero factor in the quoted bound when \(|\Gamma_t|=0\). No singleton-domain exception is missing: differing outcomes necessarily differ on a nonsingleton domain.
Summing the nonempty-premise bounds over explicitly supported types uses \(\sum_t|\Gamma_t|=s\). The inequality \(\bar d\le d\) is valid. The added \(\tau\) term covers empty-premise tests and per-type bookkeeping, yielding the stated conservative bound \(O(m^2d(s+\tau))\).
Computing one entailment bit for each listed type exactly matches the definition of \(M_\mu\). No enumeration of unlisted types or outcomes is required.
Every input denominator \(b_t\) is positive, so \(Q=\prod_t b_t\) is positive and every quotient \(Q/b_t\) is an integer. Substituting the input fractions into the definition of \(M_\mu\) verifies the displayed identity \(M_\mu=A/Q\).
Reduction of input fractions is unnecessary. The argument remains valid when denominators equal one.
The bound \(\ell(Q)\le1+\sum_t\ell(b_t)=O(L)\) is correct. The normalization promise gives exactly the identity used by the prover, and positivity ensures \(0\le A\le Q\).
The claim about intermediate sizes is also justified: partial denominator products do not exceed \(Q\), each nonnegative summand does not exceed \(Q\), and partial accumulated sums do not exceed \(Q\). The case \(A=0\) has a constant-length binary representation.
Schoolbook multiplication and division on these integers cost \(O(L^2)\) per operation. There are \(O(\tau)\) such operations, so \(O(\tau L^2)\) is a valid bound. Returning the unreduced fraction is an exact polynomial-length output.
Since \(Q,c>0\), cross multiplication preserves the inequality, giving exactly \(Ac\ge hQ\). Each product has \(O(L)\) bits, and the comparison fits the stated \(O(L^2)\) cost.
Equality is handled correctly. The argument also covers \(\rho=0\), \(\rho=1\), and aggregate values zero or one.
The conservative charge of \(O(L)\) bit operations per elementary discrete operation gives the stated total bound
\(O(m^2d(s+\tau)L+\tau L^2)\).
Routine input indexing fits within this bound. Explicit listing bounds all the combinatorial parameters polynomially in \(L\).
Therefore both claimed complexity conclusions follow. The final observation about NP-hardness is appropriately conditional on \(\mathrm{P}\ne\mathrm{NP}\).
No additional clarification or repair 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.