← back to the atlas

d4-conf-aaai-2017-0352 (d4-conf-aaai-2017-0352)

Answer: —

The anchor (named result in the paper)

Theorem 5.1 — class: algorithmic

PDF text-layer excerpt — equations and symbol order may be approximateGiven the naming game with p fraction of stubborn nodes defined above, there exists a constant p0 ≈ 0.108 such that for all 0 ≤p < p0 the expected consensus time is exp(Ω(n)). Additionally, if p0 < p ≤1 for all ϵ > 0 the fraction of original opinion is smaller than ε after O(n) steps. The proof appears in the full paper.

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

The continuous mirror question, as graded

Given a two-name complete-graph Naming Game with all ordinary agents initially holding \(\{1\}\), a rational stubborn-mass budget \(q\), tolerance \(\epsilon\), and finite horizon \(H\), what is the minimum mass \(p\le q\) to convert into stubborn agents holding \(\{0\}\) so that, under the induced mass-action flow, the mass of ordinary agents whose inventories still contain \(1\) is at most \(\epsilon\) at time \(H\)?

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

A society is given by its support: the list of the \(\tau\) types with positive mass, each mass a binary rational; \(\tau\) counts supported types, not possible types. Total mass is \(1\); initially the sole supported type is ordinary with inventory \(\{1\}\), and the number of names is \(m=2\).
Inputs are binary rationals \(0\le q\le1\), \(0<\epsilon<1\), and \(H>0\); let \(L\) be their total encoding length together with the society description. At time \(0\), choose a real mass \(p\in[0,q]\) to convert permanently into stubborn agents with inventory \(\{0\}\).
Interactions sample speaker and listener independently by mass. The speaker chooses an inventory name uniformly; recognition makes both ordinary participants retain only that name, while nonrecognition makes an ordinary listener add it. Stubborn inventories never change, in either role.
Time is normalized to one interaction per agent per unit time. Writing \(x,y,z\) for ordinary masses with inventories \(\{0\},\{1\},\{0,1\}\), respectively, the flow is \(\dot x=-xy+z^2+xz+\frac32pz\), \(\dot y=-xy+z^2+yz-py\), and \(z=1-p-x-y\), with \(x(0)=0\), \(y(0)=1-p\).
The optimization value is \(p_* = \min\{p\in[0,q]:y_p(H)+z_p(H)\le\epsilon\}\), with \(p_*=+\infty\) if this set is empty; use its exact budget-feasibility decision problem for complexity.

Is deciding whether \(p_*\le q\) in \(\mathrm P\), with running time polynomial in \(m,\tau,L\), or is it NP-hard?

For finite complete graphs, a discrete convergence result states exponential expected consensus time below a constant stubborn fraction \(p_0\approx0.108\), and reduction of the original-opinion fraction below any fixed positive tolerance in \(O(n)\) interactions above it. [Discrete result](https://ojs.aaai.org/index.php/AAAI/article/view/10621/10480).
The same mass-action equations and their equilibrium transition have been analyzed, but that analysis does not settle this exact finite-horizon budget decision problem; no result settling it was located. [Mean-field analysis](https://www.stat.berkeley.edu/users/aldous/157/Papers/social_consensus_xie.pdf).

Modeling choices made when packaging the task

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

Status

The complexity classification remains unresolved. I prove two additional finite-horizon results:

These results do not decide all exact finite-horizon comparisons, including equality. They therefore establish neither membership in $\mathrm P$ nor $\mathrm{NP}$-hardness.

Throughout, I use the prescribed initial society. Thus $m=2$ and initially $\tau=1$; the varying numerical inputs are $q,\epsilon,H$.

1. The transformed system and exact budget reduction

For a fixed converted mass $p\in[0,1]$, define

$$ r=y+z=1-p-x,\qquad s=y, $$

and write

$$ A=1+\frac p2,\qquad B=2-\frac p2. $$

Substitution into the stipulated equations gives

$$ \dot r=-Ar+Bs-s^2,\qquad \dot s=r^2-s,\qquad r(0)=s(0)=1-p. $$

The quantity tested at time $H$ is exactly $r_p(H)$.

Global existence and the physical domain

The original ordinary-agent simplex is

$$ x,y,z\ge0,\qquad x+y+z=1-p. $$

On its three boundary faces, the corresponding inward derivatives are

$$ \left.\dot x\right|_{x=0}=z^2+\frac32pz\ge0, $$

$$ \left.\dot y\right|_{y=0}=z^2\ge0, $$

$$ \left.\dot z\right|_{z=0}=2xy+py\ge0. $$

These inequalities imply forward invariance: the locally Lipschitz vector field lies in the tangent cone of the simplex at every boundary point. Compactness then prevents finite-time escape. Consequently, the solution exists uniquely for all nonnegative times, and

$$ 0\le s_p(t)\le r_p(t)\le1-p. $$

Strict monotonicity in the converted mass

Let $p_1<p_2$, put $\delta=p_2-p_1$, and define

$$ R=r_{p_1}-r_{p_2},\qquad S=s_{p_1}-s_{p_2}. $$

Subtracting the two systems yields

$$ \dot R =-A_{p_1}R+ \bigl(B_{p_1}-s_{p_1}-s_{p_2}\bigr)S +\frac{\delta}{2}(r_{p_2}+s_{p_2}), $$

$$ \dot S=(r_{p_1}+r_{p_2})R-S. $$

The off-diagonal coefficients are nonnegative. Indeed,

$$ B_{p_1}-s_{p_1}-s_{p_2} \ge B_{p_1}-(1-p_1)-(1-p_2) =\frac{p_1}{2}+p_2\ge0. $$

The forcing is nonnegative, and $R(0)=S(0)=\delta>0$. Integrating-factor formulas show that neither coordinate can have a first zero: at such a zero, its formula would still contain a strictly positive initial term and a nonnegative integral. Hence $R,S>0$. In particular,

$$ \dot R\ge-A_{p_1}R, $$

so

$$ r_{p_1}(t)-r_{p_2}(t) \ge(p_2-p_1)e^{-(1+p_1/2)t}>0. $$

Dependence on $p$ is continuous. For example, on $[0,1]^2$ the transformed fields are uniformly $4$-Lipschitz in the maximum norm, and their difference at a fixed state is at most $|p_1-p_2|$. Gronwall’s inequality gives

$$ \|(r_{p_1},s_{p_1})(t)-(r_{p_2},s_{p_2})(t)\|_\infty \le |p_1-p_2| \left(e^{4t}+\frac{e^{4t}-1}{4}\right). $$

Since $r_0(H)=1$ and $r_1(H)=0$, continuity and strict monotonicity imply a unique fraction $\beta\in(0,1)$ with $r_\beta(H)=\epsilon$. The feasible fractions in $[0,1]$ are precisely $[\beta,1]$. Therefore,

$$ \boxed{p_*\le q\quad\Longleftrightarrow\quad r_q(H)\le\epsilon.} $$

This reduction is exact, but it does not itself settle the complexity of the remaining comparison.

2. Monotone trajectories and the equilibrium transition

Fix $0<p<1$. Define

$$ g=-\dot r,\qquad w=-\dot s=s-r^2. $$

Differentiation gives

$$ \dot g=-Ag+(B-2s)w,\qquad \dot w=2rg-w. $$

On the physical domain,

$$ B-2s\ge B-2(1-p)=\frac32p>0. $$

Initially,

$$ g(0)=0,\qquad w(0)=p(1-p)>0, $$

and

$$ \dot g(0)=\frac32p^2(1-p)>0. $$

Thus both coordinates are positive for sufficiently small positive times. Their integrating-factor formulas prevent any later first zero. Consequently,

$$ g(t)>0,\qquad w(t)>0\qquad(t>0). $$

In particular, $r$ and $s$ strictly decrease at positive times, and

$$ s(t)\ge r(t)^2. $$

Their bounded monotone coordinates converge. Their limiting state is an equilibrium: otherwise, continuity of the vector field would force some coordinate to keep changing at a rate bounded away from zero.

At an equilibrium, $s=r^2$, and

$$ 0=-Ar+Br^2-r^4=-rC_p(r), $$

where

$$ C_p(r)=r^3-Br+A. $$

The minimum of this cubic on the nonnegative half-line occurs at

$$ \rho_p=\sqrt{\frac B3}, $$

and has value

$$ d_p=A-2\rho_p^3. $$

Define the integer polynomial

$$ Q(p)=2p^3+3p^2+204p-20. $$

Direct expansion gives

$$ d_p(A+2\rho_p^3)=\frac{Q(p)}{108}. $$

The second factor is positive. Also,

$$ Q'(p)=6p^2+6p+204>0. $$

The exact evaluations

$$ Q\left(\frac{39}{400}\right) =-\frac{2548081}{32000000}<0, $$

$$ Q\left(\frac{49}{500}\right) =\frac{1418399}{62500000}>0 $$

show that there is a unique critical fraction $p_c$ satisfying

$$ Q(p_c)=0,\qquad \frac{39}{400}<p_c<\frac{49}{500}<\frac1{10}. $$

For $p>p_c$, we have $d_p>0$, so the cubic has no nonnegative root. The limiting equilibrium is therefore $(0,0)$.

For $0<p\le p_c$, let $R_+(p)$ be the largest nonnegative root of $C_p$. It satisfies

$$ \rho_p\le R_+(p)<1-p. $$

Indeed, $C_p(\rho_p)\le0$, the cubic is strictly increasing above $\rho_p$, and

$$ C_p(1-p)=p^2\left(\frac52-p\right)>0. $$

Moreover, $\rho_p<5/6<1-p$, since $p\le p_c<1/10$.

The equilibrium $(R_+,R_+^2)$ lies strictly below the initial state in both coordinates. Differences between the trajectory and this equilibrium satisfy

$$ \dot R=-AR+(B-s-R_+^2)S,\qquad \dot S=(r+R_+)R-S. $$

Both off-diagonal coefficients are nonnegative, because $s,R_+^2\le1-p$. Strictly positive initial differences remain positive by the integrating-factor argument. Thus $r(t)>R_+$ at every finite time. The limiting equilibrium must consequently have $r$-coordinate $R_+$.

We have proved

$$ \lim_{t\to\infty}r_p(t)= \begin{cases} R_+(p),&0<p\le p_c,\\ 0,&p>p_c. \end{cases} $$

Finally, $p_c$ is irrational. By the rational-root theorem, a rational root of $Q$ in lowest terms has denominator dividing $2$. No positive such rational lies in $(0,1/10)$. Hence a rational budget never equals the critical fraction. This excludes equality with the *critical parameter*, but does not exclude $r_q(H)=\epsilon$.

3. New rational bounds for reaching a tolerance

The following function supplies a useful finite-horizon estimate:

$$ V=r+Bs. $$

Its derivative is

$$ \dot V=-Ar+Br^2-s^2. $$

Since $s\ge r^2$,

$$ \boxed{\dot V\le-rC_p(r).} $$

Initially,

$$ V(0)=(1+B)(1-p)\le3. $$

Below the transition

Suppose

$$ 0<p\le p_c,\qquad \epsilon>R_+(p). $$

If $\epsilon\ge1-p$, feasibility holds immediately. Otherwise, while $r(t)\ge\epsilon$, we have

$$ r(t)\ge\epsilon>R_+(p)\ge\rho_p. $$

The cubic increases above $\rho_p$, so

$$ r(t)C_p(r(t))\ge\epsilon C_p(\epsilon)>0. $$

Consequently,

$$ \dot V\le-\epsilon C_p(\epsilon) $$

until the tolerance is reached. If $r(H)\ge\epsilon$ and

$$ H\ge\frac{(1+B)(1-p)}{\epsilon C_p(\epsilon)}, $$

monotonicity ensures $r(t)\ge\epsilon$ throughout $[0,H]$, and integration gives $V(H)\le0$. This contradicts $V(H)\ge r(H)\ge\epsilon>0$.

Therefore,

$$ \boxed{ H\ge\frac{(1+B)(1-p)}{\epsilon C_p(\epsilon)} \quad\Longrightarrow\quad r_p(H)<\epsilon } $$

under the stated hypotheses.

This supplies a new polynomial-time sufficient test using only rational arithmetic. For rational $q$ with $0<q<p_c$, the required condition $\epsilon>R_+(q)$ is equivalent to

$$ \epsilon^2>\frac{4-q}{6} \qquad\text{and}\qquad C_q(\epsilon)>0. $$

To verify this equivalence, the first inequality says $\epsilon>\rho_q$. On that interval, strict increase of the cubic makes its positive sign equivalent to $\epsilon>R_+(q)$.

Thus the following entirely rational conditions imply feasibility:

$$ Q(q)<0,\qquad \epsilon^2>\frac{4-q}{6},\qquad C_q(\epsilon)>0, $$

$$ H\epsilon C_q(\epsilon)\ge(1+B_q)(1-q). $$

Conversely, for $0<q<p_c$, the conditions

$$ \epsilon^2\le\frac{4-q}{6} \qquad\text{or}\qquad C_q(\epsilon)\le0 $$

are equivalent to $\epsilon\le R_+(q)$ and therefore imply infeasibility at every finite horizon.

Above the transition

For $p>p_c$, $C_p(r)\ge d_p>0$ for every nonnegative $r$. The same argument gives

$$ H\ge\frac{(1+B)(1-p)}{\epsilon d_p} \quad\Longrightarrow\quad r_p(H)<\epsilon. $$

Moreover,

$$ A+2\rho_p^3<3, $$

so the identity relating $d_p$ and $Q(p)$ implies

$$ d_p\ge\frac{Q(p)}{324}. $$

A rational sufficient feasibility test is therefore

$$ \boxed{ Q(q)>0,\qquad H\epsilon Q(q)\ge324(1+B_q)(1-q) \quad\Longrightarrow\quad r_q(H)<\epsilon. } $$

All displayed rational tests have polynomial bit complexity in $L$: they use a fixed number of additions, multiplications, and exact comparisons of rational expressions of fixed degree. They are sufficient decision regions, not a complete algorithm.

4. New matching bounds near the transition

For $p>p_c$ and $0<\epsilon<1-p$, define the first hitting time

$$ T(p,\epsilon)=\inf\{t\ge0:r_p(t)\le\epsilon\}. $$

The preceding bound makes this time finite. Continuity and strict decrease give

$$ r_p(T(p,\epsilon))=\epsilon. $$

The main new quantitative result is the following.

Proposition. If

$$ p_c<p\le\frac1{10},\qquad \delta=p-p_c, $$

then

$$ \boxed{ \frac{1}{2\sqrt{\delta}} \le T\left(p,\frac12\right) \le\frac{144}{\sqrt{\delta}}. } $$

Thus the time needed to reach the fixed tolerance $1/2$ is bounded above and below by constant multiples of $\delta^{-1/2}$.

4.1. A scalar speed bound

Write

$$ h(r)=rC_p(r),\qquad \kappa=p\left(\frac52-p\right)>0. $$

Using $s=r^2+w$ in the equation for $r$ gives

$$ g=-\dot r=h(r)-(B-s-r^2)w. $$

The physical bounds imply

$$ B-s-r^2 \ge B-(1-p)-(1-p)^2 =\kappa. $$

Since $g,w\ge0$,

$$ 0\le g\le h(r),\qquad 0\le w\le\frac{h(r)}{\kappa}. $$

These inequalities will give the lower bound and control the upper-bound calculation.

4.2. The lower bound

The cubic has the exact expansion

$$ C_p(r)=d_p+(r-\rho_p)^2(r+2\rho_p). $$

Differentiating its minimum value gives

$$ d_p'=\frac{1+\rho_p}{2}. $$

Because $d_{p_c}=0$ and $0<\rho_p<1$,

$$ \frac{\delta}{2}\le d_p\le\delta. $$

Our range of $p$ also gives

$$ 0<\delta<\frac1{400},\qquad \frac34<\rho_p<\frac56. $$

The interval

$$ [\rho_p-\sqrt{\delta},\,\rho_p+\sqrt{\delta}] $$

lies strictly between $1/2$ and the initial value $1-p$. Indeed,

$$ \rho_p-\sqrt{\delta}>\frac34-\frac1{20}>\frac12, $$

$$ \rho_p+\sqrt{\delta}<\frac56+\frac1{20}<\frac9{10}\le1-p. $$

The trajectory must cross this interval before reaching $1/2$.

Within it, writing $u=r-\rho_p$, we have

$$ C_p(r) =d_p+u^2(3\rho_p+u) \le \delta+\delta\left(\frac52+\frac1{20}\right) <4\delta. $$

Because $r\le1$, the speed bound gives

$$ -\dot r=g\le rC_p(r)<4\delta. $$

Crossing an interval of width $2\sqrt{\delta}$ therefore takes at least

$$ \frac{2\sqrt{\delta}}{4\delta} =\frac1{2\sqrt{\delta}}. $$

This proves the lower bound.

4.3. An upper hitting-time estimate

I first prove a bound valid for every $p>p_c$ and $0<\epsilon<1-p$:

$$ T(p,\epsilon) \le \frac{5\pi}{\epsilon\sqrt{d_p}} + \frac{B}{\kappa} \left( 1+2\log\frac{3}{\epsilon d_p} \right). $$

Set $T=T(p,\epsilon)$ and observe that

$$ V=r+Bs=r+Br^2+Bw. $$

Since $-\dot V\ge h(r)>0$,

$$ T\le\int_0^T\frac{-\dot V}{h(r)}\,dt. $$

Substituting the expression for $V$ and using $g=-\dot r$ gives

$$ T \le \int_\epsilon^{1-p} \frac{1+2Br}{rC_p(r)}\,dr + B\int_0^T\frac{-\dot w}{h(r)}\,dt. $$

The first integral is bounded by

$$ \frac5\epsilon\int_\epsilon^{1-p}\frac{dr}{C_p(r)}. $$

The cubic expansion and $2\rho_p>1$ imply

$$ C_p(r)\ge d_p+(r-\rho_p)^2. $$

Extending the integral to the real line therefore gives

$$ \int_\epsilon^{1-p} \frac{1+2Br}{rC_p(r)}\,dr \le \frac5\epsilon \int_{-\infty}^{\infty}\frac{du}{d_p+u^2} = \frac{5\pi}{\epsilon\sqrt{d_p}}. $$

It remains to bound the integral involving $\dot w$. Let

$$ u(t)=\frac1{h(r(t))}. $$

Integration by parts yields

$$ \int_0^T\frac{-\dot w}{h(r)}\,dt = \frac{w(0)}{h(r(0))} -\frac{w(T)}{h(\epsilon)} +\int_0^T w(t)\dot u(t)\,dt. $$

The middle term is nonpositive. Furthermore,

$$ \frac{w(0)}{h(r(0))} = \frac{p(1-p)} {(1-p)p^2(5/2-p)} =\frac1\kappa. $$

On intervals where $\dot u>0$, the bound $w\le h/\kappa$ gives

$$ w\dot u \le\frac1\kappa\frac{\dot u}{u} =\frac1\kappa\frac{d}{dt}\log u. $$

Terms where $\dot u\le0$ can be discarded in an upper bound.

To count the increasing intervals of $u$, calculate

$$ h'(r)=4r^3-2Br+A,\qquad h''(r)=12r^2-2B. $$

On the nonnegative half-line, $h'$ first decreases and then increases. Hence $h'>0$ on at most two intervals. Because $r$ decreases, these give at most two intervals where $u$ increases.

Throughout $[0,T]$,

$$ \epsilon d_p\le h(r(t))\le3. $$

Each increasing interval of $\log u$ contributes at most

$$ \log\frac{3}{\epsilon d_p}. $$

Therefore,

$$ \int_0^T\frac{-\dot w}{h(r)}\,dt \le \frac1\kappa \left( 1+2\log\frac{3}{\epsilon d_p} \right), $$

which proves the asserted general upper estimate.

4.4. Specializing the upper bound

Now take $\epsilon=1/2$ and $p_c<p\le1/10$. We have

$$ d_p\ge\frac{\delta}{2}, $$

and

$$ \kappa =p\left(\frac52-p\right) > \frac{39}{400}\cdot\frac{12}{5} >\frac15. $$

Since $B\le2$, the general estimate implies

$$ T\left(p,\frac12\right) \le \frac{10\pi\sqrt2}{\sqrt{\delta}} + 10\left(1+2\log\frac{12}{\delta}\right). $$

For $x\ge1$, $\log x\le\sqrt x$. One way to verify this is to maximize $(\log x)/\sqrt x$; its maximum is $2/e<1$. Consequently,

$$ \sqrt{\delta}\,T\left(p,\frac12\right) \le 10\pi\sqrt2+10\sqrt{\delta}+20\sqrt{12}. $$

Using $\pi<4$, $\sqrt2<3/2$, $\sqrt{12}<7/2$, and $\sqrt{\delta}<1/20$, the right side is less than

$$ 60+\frac12+70<144. $$

This completes the proof of the proposition.

5. Consequences for binary inputs

Exact rational tests near the transition

For $p_c<q\le1/10$, the derivative bounds

$$ 204\le Q'(p)\le205 $$

and the mean-value theorem give

$$ 204(q-p_c)\le Q(q)\le205(q-p_c). $$

Combining these inequalities with the hitting-time proposition gives

$$ T\left(q,\frac12\right) \ge\frac{\sqrt{204}}{2\sqrt{Q(q)}} >\frac7{\sqrt{Q(q)}}, $$

and

$$ T\left(q,\frac12\right) \le\frac{144\sqrt{205}}{\sqrt{Q(q)}} <\frac{2304}{\sqrt{Q(q)}}. $$

Thus, for tolerance $\epsilon=1/2$ and budgets satisfying $Q(q)>0$ and $q\le1/10$,

$$ \boxed{ H^2Q(q)\le49 \quad\Longrightarrow\quad p_*>q, } $$

$$ \boxed{ H^2Q(q)\ge2304^2 \quad\Longrightarrow\quad p_*\le q. } $$

These are exact polynomial-time tests using rational arithmetic. They leave the intervening range unresolved.

Exponentially long hitting times with short descriptions

For an integer $k\ge10$, define the dyadic rational

$$ q_k=\frac{\lceil2^kp_c\rceil}{2^k}. $$

Irrationality of $p_c$ implies

$$ 0<q_k-p_c<2^{-k}. $$

Also, $q_k<1/10$ for $k\ge10$, because $p_c<49/500$.

The integer $\lceil2^kp_c\rceil$ can be computed in polynomial time in $k$: binary search among the dyadic grid points uses $O(k)$ exact sign comparisons of the fixed-degree polynomial $Q$ on $O(k)$-bit rationals.

The lower hitting-time bound gives

$$ T\left(q_k,\frac12\right)>2^{k/2-1}. $$

Choose

$$ H_k=2^{\lfloor k/2\rfloor-2}. $$

Then

$$ r_{q_k}(H_k)>\frac12, $$

so these instances are infeasible despite $q_k>p_c$. Their total encoding length is $\Theta(k)$, while their time to reach tolerance $1/2$ is at least exponential in that length.

This is not a computational lower bound. An algorithm could exploit the equations without simulating every elapsed unit of time. The construction only rules out an argument that truncates all above-transition trajectories at a horizon polynomial in the input length.

6. What remains open

The exact decision problem is still

$$ r_q(H)\le\epsilon. $$

The new bounds decide additional substantial regions and quantify the delay near the transition. They do not settle comparisons in the remaining regions.

In particular:

The supplied [mean-field analysis](https://www.stat.berkeley.edu/users/aldous/157/Papers/social_consensus_xie.pdf) studies the equilibrium transition, while the [discrete convergence result](https://ojs.aaai.org/index.php/AAAI/article/view/10621/10480) concerns stochastic finite-population dynamics. Neither substitutes for an exact bit-complexity analysis of this finite-horizon comparison.

⟨structured verdict parsed — rendered above⟩

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

Verification report

Assessment: correct partial progress; the requested complexity classification remains unresolved. The reductions, sufficient tests, and hitting-time estimates withstand verification. I found no mathematical error in those results. The blocking issue is completeness: neither a polynomial-time algorithm for every allowed input nor a hardness reduction is provided.

The prover accurately acknowledges this limitation. Accordingly, the output is partial, rather than a refuted proof or a completed solution.

1. Transformed system and budget reduction

The substitution $r=1-p-x$ and $s=y$ correctly gives

$$ \dot r=-Ar+Bs-s^2,\qquad \dot s=r^2-s, $$

with the stated coefficients and initial conditions.

The three boundary derivatives are correct. The vector field is polynomial and therefore locally Lipschitz; its inward directions on the faces satisfy the stated tangent-cone criterion. Forward invariance and compactness justify unique global solutions in the physical domain, including the endpoint parameters $p=0$ and $p=1$.

The equations for the parameter differences $R,S$ are correct. In particular,

$$ B_{p_1}-s_{p_1}-s_{p_2}\ge \frac{p_1}{2}+p_2\ge0. $$

The integrating-factor argument legitimately excludes a first zero because both initial differences are strictly positive. The subsequent lower bound on $R$ follows from the displayed differential inequality.

The claimed uniform Lipschitz and parameter-dependence bounds are valid on the stated square. Consequently, the continuity argument, endpoint values, and strict monotonicity establish a unique threshold $\beta$. This proves the exact equivalence

$$ p_*\le q\quad\Longleftrightarrow\quad r_q(H)\le\epsilon. $$

The definition $p_*=+\infty$ for an empty feasible set is handled correctly by this equivalence.

Finding: this section is rigorous and establishes a genuine reduction of the optimization decision to one trajectory comparison.

2. Monotone trajectories and equilibrium transition

For $0<p<1$, the differentiated equations for $g,w$ and their initial values are correct. The positive off-diagonal coefficients and integrating-factor argument establish positivity at every positive time. Hence both trajectory coordinates strictly decrease, and $s\ge r^2$.

The argument that their limit is an equilibrium is valid: a nonzero limiting derivative would contradict convergence of the corresponding coordinate.

The equilibrium cubic and its minimum are correct. I independently checked the polynomial identity and rational evaluations:

$$ 108\left(A^2-4\left(\frac B3\right)^3\right) =2p^3+3p^2+204p-20, $$

$$ Q\left(\frac{39}{400}\right) =-\frac{2548081}{32000000}, \qquad Q\left(\frac{49}{500}\right) =\frac{1418399}{62500000}. $$

Together with strict increase of $Q$, these establish the claimed critical parameter.

Below and at the transition, the location of $R_+$ and the comparison with its equilibrium are valid. The difference system has nonnegative off-diagonal coefficients on the physical domain. Its strictly positive initial differences therefore remain positive. Since no larger nonnegative equilibrium root exists, the limiting trajectory must have $r$-coordinate $R_+$.

The rational-root argument correctly proves irrationality of $p_c$. The prover also correctly limits its consequence: this excludes a rational budget equal to $p_c$, but says nothing about finite-time equality with the tolerance.

Finding: the equilibrium classification and trajectory limits are established.

3. Rational sufficient tests

The derivative of $V=r+Bs$ is correct, and $s\ge r^2$ gives

$$ \dot V\le-rC_p(r). $$

Below the transition, the lower bound on $rC_p(r)$ applies throughout the interval before reaching the tolerance. The contradiction obtained by integrating under the hypothesized failure at time $H$ is valid. The displayed weak inequality on the horizon still yields a strict conclusion because $V(H)\ge\epsilon>0$ contradicts $V(H)\le0$.

The rational characterization of $\epsilon>R_+(q)$ is correct. Its complement is also correctly expressed by the stated disjunction. Since finite-time trajectories remain strictly above $R_+$, this complement implies finite-horizon infeasibility.

Above the transition, $C_p(r)\ge d_p>0$ justifies the analogous bound. The estimate $A+2\rho_p^3<3$ holds on the relevant parameter range, and the conversion to the bound involving $Q$ is valid.

The polynomial bit-complexity claim applies to these tests: each evaluates a fixed number of rational expressions of fixed degree. It does not imply a complete polynomial-time decision algorithm, and the prover does not claim otherwise.

Finding: these are valid sufficient decision regions.

4. Hitting-time bounds

Scalar speed estimate

The identity involving $g,h,w$ is correct. The physical-domain estimate

$$ B-s-r^2\ge p\left(\frac52-p\right)=\kappa $$

justifies both $g\le h(r)$ and $w\le h(r)/\kappa$.

Lower bound

The cubic expansion and derivative of $d_p$ are correct. The resulting bounds on $d_p$, $\delta$, and $\rho_p$ justify the location of the crossing interval.

Within that interval, the stated bound $C_p(r)<4\delta$ is valid. The speed estimate therefore gives the claimed lower bound on its crossing time, and hence on the hitting time.

General upper bound

The substitution into the integral involving $-\dot V$ is valid. The trajectory is strictly decreasing at positive times, so the change of variable in the first integral is justified.

For every admissible parameter in this argument, $2\rho_p>1$. Thus the quadratic lower bound on the cubic and the integral over the real line give the stated first-term estimate.

The integration-by-parts identity for the second term has the correct signs. The initial boundary contribution equals $1/\kappa$, and the final contribution is nonpositive.

The interval-counting argument is also correct: $h'$ decreases and then increases on the nonnegative half-line, so its positive set has at most two intervals. Since $r$ decreases, these correspond to at most two increasing intervals of $u=1/h(r)$. The bounds on $h$ control the logarithmic increase on each interval.

Specialization

The estimates on $\kappa$, $B$, and $d_p$ are valid. The logarithmic inequality applies because its argument exceeds $1$. The final numerical estimates indeed give a constant strictly below $144$.

Finding: the proposition’s upper and lower bounds, including their constants, are established.

5. Binary-input consequences

The derivative bounds for $Q$ hold on the specified interval. Their combination with the hitting-time proposition gives the stated inequalities involving $Q(q)$; the inequality directions are correct.

The rational horizon tests correctly handle their boundary comparisons. In particular, the strict lower hitting-time bound makes the stated infeasibility test valid even when its rational comparison is an equality.

The dyadic construction is valid. Irrationality gives strict rounding above $p_c$, and the supplied bound on $p_c$ places every specified budget below $1/10$. Binary search using exact signs of $Q$ has polynomial bit complexity.

The chosen horizons lie strictly below the proven hitting-time lower bounds. Their encoding length, together with that of the budgets, is $\Theta(k)$. Thus the examples do establish exponentially long physical hitting times for inputs of linear encoding length.

The prover correctly states that this is not a computational lower bound.

Finding: these consequences follow from the verified estimates.

6. Outstanding issue and minimum required continuation

Major scope issue: the assigned decision problem is still unanswered. The output establishes only partial decision regions and trajectory estimates.

To resolve the assignment, a subsequent output must provide either:

The write-up itself needs no mathematical repair for the partial results audited above. Further progress requires an additional argument addressing the unresolved comparisons.

The supplied references support the distinction between mean-field equilibrium analysis and stochastic finite-population dynamics; neither is used here as a substitute for the missing exact complexity argument. [Mean-field analysis](https://www.stat.berkeley.edu/users/aldous/157/Papers/social_consensus_xie.pdf), [discrete analysis](https://ojs.aaai.org/index.php/AAAI/article/view/10621/10480).

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