Answer: —
Theorem 1 — class: other
PDF text-layer excerpt — equations and symbol order may be approximateGiven a task j (1 ≤j ≤n) processed by m workers, we can obtain an answer set Xj = {xij|i ≤m}. For simplicity, we use l to mark xij. Worker i has ability πij = [πij kl] when processing task j, πij kl is the performance when worker i processes task j the truth answer of which is k ∈A. Let f(Xj) denote the aggregation method.
statement extracted from the paper’s text layer; consult the paper for the exact wording
Given a worker pool of size \(N\), rational type fractions \(\mu_t\) over a finite set \(T\), each type’s response model, a task-label distribution, an aggregation rule, and targets \(\epsilon,\eta,\delta\), choose a common participation share \(\alpha\in[0,1]\) and task intensity \(r\ge 0\) to minimize \(Q=N\alpha r\). Require the paper’s guarantees that the learned aggregator disagrees with the target rule on at most an \(\epsilon\) fraction of tasks with probability at least \(1-\delta\), and that the aggregation error is at most \(\eta\); report infeasibility if the available pool cannot meet them.
A society is given by its support: the list of \(\tau\) types with positive binary-rational masses \(\mu_t\), summing to \(1\); \(\tau\) is the support size, not the number of possible types.
There are \(m\ge2\) labels, a pool capacity \(N\in\mathbb N_{>0}\), and a rational task-label distribution \(D\). Type \(t\) has a task-independent rational confusion matrix \(\pi_t\), with nonnegative entries and row sums \(1\); responses are conditionally independent given the true label and worker types.
The target aggregator maximizes the sum of rational scores \(S_t(k,l)\in[a,b]\), where \(a<b\), breaking ties by the smallest label. Its finite realizable hypothesis class has supplied cardinality \(H\ge1\); an input flag specifies whether parameter learning is required.
For every true label \(k\) with \(D_k>0\) and rival \(g\ne k\), define \(d_{tkg}=\sum_l\pi_t(k,l)(S_t(k,l)-S_t(g,l))\), \(M_{kg}=\sum_t\mu_t d_{tkg}\), and \(V_{kg}=\sum_t\mu_t(d_{tkg}-M_{kg})^2\). Assume \(M_{kg}>0\) for all these pairs.
Use the certified-quality formulation: fractional worker and task counts extend the numerical query guarantees to real arguments. Choose \(\alpha\in(0,1]\) and \(r>0\), put \(s=N\alpha\), and minimize \(Q=sr\).
For binary-rational targets \(\epsilon,\eta\in(0,1/2)\) and \(\delta\in(0,1/4)\), aggregation certification requires \(sM_{kg}^2\ge2(b-a)^2\ln((m-1)/\eta)+V_{kg}\) for every relevant pair. Learning certification requires \(r\ge2\ln(2H/\delta)/(\epsilon^2(1-2\eta)^2)\); when no learning is required, use \(r\ge1\). These certify target-rule disagreement at most \(\epsilon\) with confidence \(1-\delta\), and the aggregation-quality bound at most \(\eta\).
Given a nonnegative binary-rational budget \(B\), is deciding whether such a certified allocation exists with \(Q\le B\) in polynomial time, or is it NP-hard? State running times in \(m\), \(\tau\), total input bit length \(L\), and \(\log N\) and \(\log H\).
The discrete analogue has a published closed-form query-cost bound combining worker-score moments with a finite-class PAC sample bound; this is a query guarantee, not a computational runtime classification. [Verified source](https://www.ijcai.org/proceedings/2018/0212.pdf)
No result settling exactly this fractional certified-allocation decision problem was identified in the literature search.
Partial resolution. I prove polynomial-time solvability without learning, and with learning whenever the two rational logarithm arguments are multiplicatively dependent. This extends the equal-argument learning case in the notes. For arbitrary learning inputs, I reduce the remaining decision to one scalar logarithm-product comparison, but do not prove a polynomial-time algorithm or NP-hardness.
I use the standard Turing model and assume that $a,b$ are rational input parameters or fixed rational constants. All allocation variables are real, as stipulated.
Write
$$
T=2+L+\left\lceil\log_2(N+1)\right\rceil+
\left\lceil\log_2(H+1)\right\rceil.
$$
If $L$ already includes the encodings of $N,H$, then $T=O(L)$. The polynomial-time results below have bit running time
$$
O\!\left(\tau m^3\operatorname{poly}(T)\right).
$$
They use only the supplied support and do not enumerate workers or hypotheses.
The cited [IJCAI paper](https://www.ijcai.org/proceedings/2018/0212.pdf) studies query-cost guarantees. Here the computational problem is deciding the certification inequalities supplied in the question.
Let
$$
\mathcal I=\{(k,g):D_k>0,\ g\ne k\}.
$$
This set is nonempty: some $D_k$ is positive, and $m\ge2$.
Define
$$
w=b-a,\qquad c=2w^2,\qquad
A=\frac{m-1}{\eta},\qquad C=\frac{2H}{\delta},
$$
and put
$$
x=\ln A,\qquad y=\ln C.
$$
The hypotheses imply $w>0$, $A>2$, and $C>8$, so $x,y>0$.
For $i=(k,g)\in\mathcal I$, define the rational numbers
$$
\lambda_i=\frac{c}{M_{kg}^2},
\qquad
\nu_i=\frac{V_{kg}}{M_{kg}^2}.
$$
Thus $\lambda_i>0$ and $\nu_i\ge0$. Set
$$
s_*=\max_{i\in\mathcal I}(\lambda_i x+\nu_i).
$$
For the minimum certified task count, set $R=1$ without learning; with learning, set
$$
\gamma=\frac{2}{\epsilon^2(1-2\eta)^2},
\qquad R=\gamma y.
$$
Proposition 1. A certified allocation within budget exists exactly when
$$
s_*\le N
\qquad\text{and}\qquad
s_*R\le B.
$$
If the pool constraint is feasible, the minimum certified cost is attained and equals $s_*R$.
Proof. The permitted worker counts are exactly $0<s\le N$, since $s=N\alpha$ and $0<\alpha\le1$.
Dividing each aggregation inequality by its positive $M_{kg}^2$ shows that all aggregation constraints hold exactly when $s\ge s_*$. Task certification holds exactly when $r\ge R$. Since $s_*,R>0$, every certified allocation satisfies
$$
sr\ge s_*R.
$$
Conversely, if the two displayed inequalities hold, choose
$$
s=s_*,\qquad r=R,\qquad \alpha=\frac{s_*}{N}.
$$
These choices satisfy every constraint and attain cost $s_*R$. $\square$
In particular, $B=0$ is always infeasible.
Every score difference lies in $[-w,w]$. Taking its expectation therefore gives
$$
-w\le d_{tkg}\le w.
$$
Because $M_{kg}>0$, it follows that $0<M_{kg}\le w$. Expanding the variance gives
$$
V_{kg}
=\sum_t\mu_t d_{tkg}^2-M_{kg}^2
\le w^2-M_{kg}^2.
$$
Consequently,
$$
\lambda_i\ge2,
\qquad
0\le\nu_i\le\frac{\lambda_i}{2}-1.
$$
In particular,
$$
0\le\frac{\nu_i}{\lambda_i}
=\frac{V_{kg}}{2w^2}
\le\frac12-\frac1{\lambda_i}<\frac12.
$$
These restrictions will apply to the scalar comparison obtained below.
There are at most $m(m-1)$ relevant pairs. Computing each $d_{tkg}$ requires a sum over $m$ responses, so all margins and moments can be computed using
$$
O(\tau m^3)
$$
rational arithmetic operations. The variance identity used above follows directly from
$$
\sum_t\mu_t=1,
\qquad
\sum_t\mu_t d_{tkg}=M_{kg}.
$$
All rational preprocessing outputs have $O(T)$ bits. To verify this, let $P$ be the product of all rational input denominators. Its bit length is $O(T)$. The margins and moments are polynomials of bounded degree in the input entries; their denominators therefore divide a fixed power of $P$. Their numerators also have $O(T)$ bits: input magnitudes are bounded exponentially in $T$, and only polynomially many terms are summed. The divisions defining $\lambda_i,\nu_i,\gamma$ preserve polynomial, indeed $O(T)$, representation size.
Thus preprocessing uses
$$
O\!\left(\tau m^3\operatorname{poly}(T)\right)
$$
bit operations.
We also need certified logarithm intervals. For a rational $z>1$, write
$$
z=2^h u,\qquad 1\le u<2,
\qquad v=\frac{u-1}{u+1}.
$$
Here $h=O(T)$ and $0\le v<1/3$. Integrating the geometric series yields
$$
\ln u
=2\sum_{j=0}^{n-1}\frac{v^{2j+1}}{2j+1}+E_n,
$$
where
$$
0\le E_n\le
\frac{2v^{2n+1}}{(2n+1)(1-v^2)}.
$$
The same formula with $v=1/3$ supplies bounds for $\ln2$. Since
$$
\ln z=h\ln2+\ln u,
$$
taking $n=O(p+\log(T+2))$ gives a rational interval of width at most $2^{-p}$. The number of terms and the bit lengths of their exact rational sums are polynomial in $T+p$.
Therefore logarithms can be enclosed to $p$ bits of absolute precision in $\operatorname{poly}(T+p)$ time. This fact alone does not establish polynomial-time exact comparison.
For an algebraic number, its ordinary height is the largest absolute coefficient of its primitive integer minimal polynomial.
Lemma 2. There is an effective absolute constant $K$ such that, for $h\ge2$, a rational $z>1$ and a real algebraic $\beta$ of degree at most $2$, both of height at most $2^h$, satisfy
$$
|\ln z-\beta|
>
2^{-K h^2\log_2(h+2)}.
$$
Proof. Equality is impossible: it would make $\beta=\ln z>0$ algebraic with algebraic exponential, contrary to Hermite–Lindemann.
Apply the quantitative theorem in [Baker, Section 3](https://www.cambridge.org/core/services/aop-cambridge-core/content/view/D0EDFA9159B2D0FE0059024F5D98CC0F/S144678870002142Xa.pdf/transcendence-theory-and-its-applications.pdf) to
$$
\Lambda=\beta-\ln z+0\ln2.
$$
Its algebraic entries generate a field of degree at most $2$; the logarithm arguments are different from $0,1$; and $\Lambda\ne0$. Choose
$$
A_1=\max(5,\operatorname{ht}(z)),\quad A_2=5,
\quad B_0=\max(5,\operatorname{ht}(\beta)).
$$
For two logarithms and bounded field degree, Baker’s bound gives
$$
|\Lambda|>
\exp\!\left[-K_1\Omega\ln\Omega'\ln(B_0\Omega)\right],
\qquad
\Omega=\ln A_1\ln A_2,\quad \Omega'=\ln A_1,
$$
with an effective absolute $K_1$. Now
$$
\Omega=O(h),\qquad
\ln\Omega'=O(\ln(h+2)),\qquad
\ln(B_0\Omega)=O(h).
$$
Combining these estimates and changing logarithm bases proves the bound. $\square$
Thus comparing $\ln z$ with a rational or quadratic algebraic number of $O(T)$-bit height requires only
$$
O(T^2\log(T+2))
$$
bits of certified precision.
Proposition 3. An index $i_0$ attaining $s_*$ can be found in polynomial time. Moreover, two worker thresholds are equal only when their rational coefficient pairs are identical.
Proof. Two thresholds differ by
$$
(\lambda_i-\lambda_j)x+(\nu_i-\nu_j).
$$
If $\lambda_i=\lambda_j$, their order is determined by rational arithmetic. Otherwise, their order is determined by comparing $x$ with the rational number
$$
q=\frac{\nu_j-\nu_i}{\lambda_i-\lambda_j},
$$
accounting for the sign of $\lambda_i-\lambda_j$.
If $q\le0$, then $x>0$ determines this comparison immediately. If $q>0$, Lemma 2 determines it in polynomial time. A tournament over the relevant pairs therefore finds a maximum.
Also, $x=\ln A$ is transcendental by Hermite–Lindemann. Hence equality of two thresholds with different slopes would make $x$ rational, which is impossible. Equality with identical slopes requires identical intercepts. $\square$
Every threshold $\lambda_i x+\nu_i$ is transcendental, since $\lambda_i$ is a nonzero rational. A finite maximum equals one of its entries, so $s_*$ is transcendental. Consequently,
$$
s_*\ne N.
$$
Equality with the pool capacity is therefore impossible.
The pool constraint is decidable in polynomial time, either using the selected index or testing
$$
x\le \min_{i\in\mathcal I}\frac{N-\nu_i}{\lambda_i}
$$
with Lemma 2.
Without learning, $R=1$. Put
$$
Z=\min(N,B),
\qquad
q=\min_{i\in\mathcal I}\frac{Z-\nu_i}{\lambda_i}.
$$
Proposition 1 gives
$$
\text{feasible}\quad\Longleftrightarrow\quad x\le q.
$$
If $q\le0$, reject. Otherwise $q$ is an $O(T)$-bit rational, and Lemma 2 decides the comparison in polynomial time.
Thus the entire no-learning case is polynomial-time solvable in
$$
O\!\left(\tau m^3\operatorname{poly}(T)\right)
$$
bit operations.
Positive rationals $A,C>1$ are multiplicatively dependent if there exist positive integers $p,q$ such that
$$
C^q=A^p.
$$
Equivalently,
$$
\ln C=\frac pq\ln A.
$$
Lemma 4. Multiplicative dependence of two positive rationals greater than $1$ can be detected in polynomial time. When dependence holds, a corresponding rational ratio of their logarithms can be found in polynomial time.
Proof. Reduce $A,C$ to lowest terms. Let all four numerators and denominators be smaller than $2^h$, with $h=O(T)$.
Suppose dependence holds, and choose relatively prime positive $p,q$ satisfying $C^q=A^p$. There is a prime $\ell$ whose valuation in $A$ is nonzero, since $A\ne1$. Write
$$
e_A=v_\ell(A),\qquad e_C=v_\ell(C).
$$
Taking valuations gives
$$
q e_C=p e_A.
$$
Since $p,q$ are relatively prime,
$$
q\mid e_A,\qquad p\mid e_C.
$$
Both valuations are nonzero and have absolute value at most $h$. Thus
$$
1\le p,q\le h.
$$
It therefore suffices to enumerate these $h^2$ pairs and test $C^q=A^p$ by exact integer arithmetic. The integers used in each test have $O(h^2)$ bits, so the search is polynomial. Prime valuations justify the bound; the algorithm does not compute them or factor either rational. $\square$
Theorem 5. With learning required, multiplicatively dependent $A,C$ give a polynomial-time decision problem.
Proof. Find $\rho=p/q>0$ using Lemma 4, so $y=\rho x$. Select a binding index $i_0$ using Proposition 3, and write
$$
\lambda=\lambda_{i_0},\qquad \nu=\nu_{i_0}.
$$
First decide the pool constraint in polynomial time. If it fails, reject.
Assume $B>0$, since zero budget is infeasible. The remaining budget inequality is
$$
a_2x^2+a_1x-B\le0,
\qquad
a_2=\gamma\rho\lambda>0,\quad
a_1=\gamma\rho\nu\ge0.
$$
The polynomial is negative at zero, tends to positive infinity, and has derivative
$$
2a_2X+a_1>0\qquad(X>0).
$$
It therefore has exactly one positive root $\beta$, and the budget condition is equivalent to $x\le\beta$.
The root is
$$
\beta=\frac{-a_1+\sqrt{a_1^2+4a_2B}}{2a_2}.
$$
Clearing denominators in its defining quadratic gives integer coefficients with $O(T)$ bits. If the quadratic is irreducible, this bounds the height of $\beta$. If $\beta$ is rational, the rational-root theorem bounds its reduced numerator and denominator by the integer coefficients. Hence $\beta$ has degree at most $2$ and height at most $2^{O(T)}$.
Certified root approximation is polynomial-time: the root lies between $0$ and
$$
U=1+\frac{B}{a_2},
$$
because $\beta^2\le B/a_2$ and $\sqrt{t}<1+t$ for $t>0$. Bisection, evaluating the quadratic exactly at rational midpoints, produces an interval of width $2^{-p}$ after $O(T+p)$ steps.
Lemma 2 now decides $x\le\beta$ with polynomial precision and time. Including preprocessing and dependence detection gives
$$
O\!\left(\tau m^3\operatorname{poly}(T)\right).
$$
$\square$
This includes $C=A$, but also every other rational power relation between $A$ and $C$.
Suppose the pool constraint passes. Select $i_0$ as above and put
$$
\lambda=\lambda_{i_0},\qquad
\nu=\nu_{i_0},\qquad
u=\frac{\nu}{\lambda},\qquad
v=\frac{B}{\gamma\lambda}.
$$
Then
$$
s_*R=\gamma\lambda(x+u)y.
$$
Therefore the remaining decision is exactly
$$
(\ln A+u)\ln C\le v.
$$
All four parameters are rational with $O(T)$-bit representations, and they satisfy
$$
A>2,\qquad C>8,\qquad 0\le u<\frac12.
$$
Thus the general allocation problem has no remaining search over allocation variables or worker constraints. Its unresolved part is one exact numerical comparison of this form.
Lemma 2 does not decide it: viewing the expression as linear in $\ln C$ gives the coefficient $\ln A+u$, which is transcendental rather than algebraic.
This numerical issue already occurs with fixed numbers of labels and types.
Take
$$
m=2,\quad \tau=1,\quad \mu_1=1,\quad D=(1,0),
$$
with identity confusion matrix, scores
$$
S_1(k,l)=\mathbf1_{\{k=l\}},
$$
and bounds $a=0,b=1$. The sole relevant pair has
$$
M_{12}=1,\qquad V_{12}=0.
$$
Set
$$
\epsilon=\eta=\frac14,\qquad H=3,\qquad N=4,
$$
and require learning. A three-rule hypothesis class can consist of the target majority rule and the two constant-label rules. It contains the target, as required by realizability.
Allow $\delta\in(0,1/4)$ to vary. Then
$$
s_*=2\ln4,\qquad
R=128\ln(6/\delta),
$$
so
$$
Q_{\min}=256\ln4\,\ln(6/\delta).
$$
The pool constraint always passes because
$$
2\ln4=4\ln2<4,
$$
where $\ln2=\int_1^2dt/t<1$.
Consequently, for a nonnegative binary-rational $q$, setting $B=256q$ gives
$$
\text{feasible}
\quad\Longleftrightarrow\quad
\ln4\,\ln(6/\delta)\le q.
$$
This transformation has polynomial bit complexity and preserves dyadic encoding if that is the intended meaning of binary-rational.
For $\delta=1/16$, the second argument is $96$. The arguments $4$ and $96$ are multiplicatively independent: $4^p=96^q$ with positive $p,q$ would contradict their prime-$3$ valuations.
This proves that a restricted logarithm-product comparison is embedded in valid allocation instances. No hardness classification for that numerical comparison is proved here.
Define
$$
F=\max\{s_*-N,\ s_*R-B\}.
$$
Feasibility is equivalent to $F\le0$.
Suppose a positive integer $p$ is given and the input is promised to satisfy
$$
F\le-2^{-p}
\qquad\text{or}\qquad
F\ge2^{-p}.
$$
Then the decision is solvable in
$$
O\!\left(\tau m^3\operatorname{poly}(T+p)\right)
$$
bit operations.
To prove this, all rational coefficients have magnitude at most $2^{O(T)}$, while $x,y=O(T)$. If approximations $\widehat x,\widehat y$ each have error at most $e\le1$, then
$$
\left|
\gamma(\lambda_i\widehat x+\nu_i)\widehat y
-\gamma(\lambda_i x+\nu_i)y
\right|
\le
\gamma\bigl[\lambda_i(x+y+1)+\nu_i\bigr]e
\le2^{O(T)}e.
$$
Worker-threshold errors have the same type of bound. Also,
$$
|\max_j a_j-\max_j b_j|
\le\max_j|a_j-b_j|.
$$
Hence precision $p+O(T)$ gives an approximation to $F$ with error less than $2^{-p-2}$, which determines its sign under the promise.
Without any separation promise, successively refine certified intervals for $F$.
The procedure terminates whenever $F\ne0$: once the interval error is smaller than $|F|/2$, it determines the sign.
Moreover, Proposition 3 showed that $s_*\ne N$. Thus
$$
F=0
\quad\Longleftrightarrow\quad
s_*<N\ \text{and}\ s_*R=B.
$$
The only inputs on which this procedure may fail to terminate are feasible inputs with exact budget equality.
In particular, the complement of the feasibility problem is recursively enumerable: on every infeasible input, $F>0$, and refinement eventually certifies this.
For multiplicatively independent arguments, I have not proved nonvanishing or a polynomial separation bound for
$$
(\ln A+u)\ln C-v.
$$
Neither separate transcendence of the logarithms nor the linear-form theorem used above supplies such a result.
For context, assume the conjecture that rationally independent logarithms of algebraic numbers are algebraically independent, as stated in [Waldschmidt, Conjecture 5.6](https://webusers.imj-prg.fr/~michel.waldschmidt/articles/pdf/AWSLecture5.pdf). For multiplicatively independent $A,C$, this would exclude equality because
$$
XY+uY-v
$$
is a nonzero polynomial with rational coefficients. The dependent case was already resolved above. Under that conjecture, interval refinement would therefore decide every valid input. This conditional argument supplies no polynomial-time bound.
The unconditional results proved here are polynomial-time algorithms for no learning and multiplicatively dependent learning arguments, polynomial-time selection of the binding worker constraint, and reduction of general learning feasibility to one exact scalar comparison. The requested classification for arbitrary learning inputs remains unresolved in this solution.
⟨structured verdict parsed — rendered above⟩
The output establishes a rigorous partial result, but does not resolve the full task. Its allocation reduction, polynomial-time algorithms for the stated special cases, and approximation results are sound. I found no false central step.
The unresolved case is learning with multiplicatively independent logarithm arguments. The prover explicitly acknowledges this limitation; it does not incorrectly claim a complete polynomial-time algorithm or an NP-hardness result.
The use of the standard Turing model and real allocation variables agrees with the intended decision problem.
The additional assumption that $a,b$ are rational input parameters or fixed rational constants is stated explicitly. This is a natural interpretation, but the task does not explicitly specify their encoding. The assumption matters because the proof subsequently treats $c=2(b-a)^2$ and the resulting coefficients as rational.
Minor issue: The claimed algorithms should remain explicitly qualified by this assumption about $a,b$. This is an input-model clarification, not a substantive mathematical defect under the intended rational-input reading.
The output correctly distinguishes the supplied certification inequalities from a computational complexity theorem about the discrete query guarantee.
Proposition 1 is correct.
The relevant pair set is nonempty because the task distribution has at least one positive entry and $m\ge2$. The assumptions give
$$ \lambda_i>0,\qquad \nu_i\ge0,\qquad s_*>0,\qquad R>0. $$
The permitted worker counts are exactly $0<s\le N$. Each aggregation inequality is equivalent to
$$ s\ge\lambda_i\ln A+\nu_i. $$
Thus the aggregation constraints jointly require $s\ge s_*$. The learning or no-learning constraint independently requires $r\ge R$. Positivity justifies the lower bound $sr\ge s_*R$.
The proposed allocation $s=s_*$, $r=R$, $\alpha=s_*/N$ verifies sufficiency and attainment whenever the pool and budget inequalities hold. No issue arises from the open lower endpoint for $\alpha$, since $s_*>0$.
The conclusion that $B=0$ is infeasible is also correct.
All displayed coefficient bounds are correct.
The score difference lies in $[-w,w]$, so its expectation does too. The promised positive margin therefore satisfies $0<M_{kg}\le w$.
The variance identity and bound
$$ V_{kg}=\sum_t\mu_t d_{tkg}^2-M_{kg}^2 \le w^2-M_{kg}^2 $$
use the normalization of the masses and the definition of the margin correctly. Consequently,
$$ \lambda_i\ge2,\qquad 0\le\nu_i\le\frac{\lambda_i}{2}-1, \qquad 0\le\frac{\nu_i}{\lambda_i}<\frac12. $$
The strict final inequality follows from $\lambda_i>0$ and its finite value.
The arithmetic-operation count $O(\tau m^3)$ is valid: there are at most $m(m-1)$ pairs, and computing their type-specific margins requires summation over $m$ responses.
The representation-size argument is sound for explicitly supplied rational inputs. The margins and moments involve bounded-degree expressions in input rationals. A fixed power of the product of input denominators bounds their denominators, and subsequent rational divisions preserve $O(T)$ bit size.
The logarithm series and its remainder bound are correct. Range reduction places $v$ in $[0,1/3)$, while the endpoint $v=1/3$ is valid for approximating $\ln2$. The stated term count accounts for multiplication of the $\ln2$ error by $h=O(T)$.
Exact summation produces rational intervals in time polynomial in $T+p$. The prover correctly cautions that computable approximations alone do not prove polynomial-time exact comparison.
Lemma 2 is supported by the cited theorem.
[Baker’s Section 3](https://www.cambridge.org/core/services/aop-cambridge-core/content/view/D0EDFA9159B2D0FE0059024F5D98CC0F/S144678870002142Xa.pdf/transcendence-theory-and-its-applications.pdf) allows an algebraic constant term in the linear form. Its hypotheses concern algebraic arguments and coefficients, their ordinary heights, the generated field degree, principal logarithms, and nonvanishing. Its bound has the dependence on $\Omega$, $\Omega'$, and the coefficient-height bound used in the output.
The application satisfies these hypotheses:
Including the zero coefficient of $\ln2$ is permitted. With $A_2=5$, the stated estimates for $\Omega$ and $\Omega'$ yield the claimed polynomial exponent.
There is therefore no unverified theorem application blocking the special-case algorithms.
Proposition 3 is correct. Different worker thresholds either have equal slopes and are compared rationally, or are ordered by a comparison of $\ln A$ with a rational number. The treatment of nonpositive comparison values is valid; positive values fall within Lemma 2.
The equality assertion is also correct: distinct rational slopes could produce equal thresholds only if $\ln A$ were rational. Hermite–Lindemann excludes this.
Each threshold is transcendental, and the finite maximum is one of those thresholds. Hence $s_*\ne N$.
Without learning, the equivalence
$$ \text{feasible}\iff \ln A\le \min_{i\in\mathcal I}\frac{\min(N,B)-\nu_i}{\lambda_i} $$
is exact. Rejection when the rational right-hand side is nonpositive is justified by $\ln A>0$. Otherwise Lemma 2 supplies polynomial-time comparison.
The claimed runtime
$$ O\!\left(\tau m^3\operatorname{poly}(T)\right) $$
is justified for this case.
Lemma 4 is correct. For a relation $C^q=A^p$ with relatively prime positive $p,q$, a nonzero prime valuation of $A$ gives
$$ qe_C=pe_A. $$
The divisibility conclusions $q\mid e_A$ and $p\mid e_C$ follow. The numerator and denominator size bounds imply $p,q\le h$, including when the chosen valuations are negative. Enumerating the bounded exponent pairs therefore detects dependence without factorization in polynomial time.
Theorem 5 correctly substitutes $y=\rho x$ and reduces the budget inequality to a quadratic in $x$. Its positive leading coefficient, nonnegative linear coefficient, and negative constant term justify the unique positive root and the comparison $x\le\beta$.
The root-height argument covers both irreducible quadratic and rational-root cases. The upper bound $U$ and rational bisection procedure are valid. Lemma 2 applies to the resulting algebraic root.
The polynomial-time claim for this learning subclass is established.
The remaining comparison
$$ (\ln A+u)\ln C\le v $$
follows exactly from the selected binding constraint. The rationality, representation sizes, and parameter restrictions stated for it are correct.
The prover correctly identifies why Lemma 2 does not directly apply: the coefficient $\ln A+u$ is transcendental.
The restricted family is internally consistent. Its sole relevant margin and variance are $M_{12}=1$ and $V_{12}=0$. The numerical constants recheck as
$$ \gamma=128,\qquad s_*=2\ln4,\qquad Q_{\min}=256\ln4\,\ln(6/\delta). $$
The pool inequality is strict. The budget transformation preserves the stated rational encoding, and the prime-$3$ valuation correctly rules out multiplicative dependence between $4$ and $96$.
This establishes an embedded numerical comparison, not a hardness result. The output accurately maintains that distinction.
The promised-gap algorithm is correct. The displayed product-error bound accounts for errors in both logarithms and their cross term. Coefficient magnitudes and logarithm sizes justify precision $p+O(T)$. The maximum operation preserves the stated uniform error control.
The interval-refinement procedure terminates whenever $F\ne0$. Since $s_*\ne N$, its characterization of possible nontermination as feasible exact-budget equality is correct. The recursive-enumerability statement is valid on the stipulated valid-input domain.
The conditional observation correctly invokes [Waldschmidt’s Conjecture 5.6](https://webusers.imj-prg.fr/~michel.waldschmidt/articles/pdf/AWSLecture5.pdf). Multiplicative independence gives rational linear independence of the two real logarithms, and the displayed polynomial is nonzero. The conclusion is explicitly conditional and supplies no polynomial runtime bound.
The established reductions and special-case results are genuine progress. Another round should focus on the stated general exact comparison rather than repeat the allocation elimination.
⟨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.