← back to the atlas

d4-conf-atal-2020-0172 (d4-conf-atal-2020-0172)

Answer: \(R=\frac12\). Acyclic instances with dyadic rational data have continuous greedy ratios arbitrarily close to \(\frac12\).

The anchor (named result in the paper)

Corollary 5.3 — class: other

PDF text-layer excerpt — equations and symbol order may be approximateThe approximation ratio of the greedy algorithm is at most 50%+ε. I.e. the approximation ratio of the greedy algorithm is tight.

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

The continuous mirror question, as graded

Given a finite type set \(T\), rational masses \(\mu_t\), message-specific contact rates \(\kappa_i(s,t)\), utilities satisfying \(\max(u_1,u_2)\le u_{1,2}\le u_1+u_2\), and a per-capita seed budget \(\beta\), determine the worst-case value ratio of marginal-gain greedy for maximizing the induced per-capita utility \(\Phi(x)\). Define the continuous greedy process as the limit of feasible mass-grid greedy allocations as the grid size tends to zero; is its infimum ratio \(1/2\), and can actual mean-field influence instances approach that ratio?

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

A society is given by its support: the list \(T\) of \(\tau\) types with positive binary-rational masses \(\mu_t\), where \(\sum_t\mu_t=1\); \(\tau\) is the support size, not the number of possible types. There are \(m=2\) messages. All contact rates \(\kappa_i(s,t)\) are nonnegative binary rationals. Utilities are common across types, rational, and satisfy \(u_1,u_2\ge0\), \(u_1+u_2>0\), and \(\max(u_1,u_2)\le u_{1,2}\le u_1+u_2\). The rational budget satisfies \(0<\beta\le1\). State any running times in \(m,\tau,L\), where \(L\) is total input bit length, and any accuracy parameters.
A feasible allocation consists of disjoint seed masses: \(x_{i,t}\ge0\), \(x_{1,t}+x_{2,t}\le\mu_t\), and \(\sum_{i,t}x_{i,t}\le\beta\). Seeds receive their assigned message certainly, and may subsequently receive the other message; allocations cannot be reassigned.
Use the following Poisson mean-field cascade. Set \(q_{i,t}^{(0)}=0\) and \(q_{i,t}^{(r+1)}=1-\exp[-\sum_s\kappa_i(s,t)(x_{i,s}+(\mu_s-x_{i,s})q_{i,s}^{(r)})]\); let \(q_{i,t}=\lim_{r\to\infty}q_{i,t}^{(r)}\). Thus \(\kappa_i(s,t)\) measures contact intensity per unit activated source mass, and the iteration selects the least fixed point.
Conditional on an individual's seed assignment, the two message cascades are independent. Define \(a_{i,t}=x_{i,t}+(\mu_t-x_{i,t})q_{i,t}\), \(b_t=x_{1,t}q_{2,t}+x_{2,t}q_{1,t}+(\mu_t-x_{1,t}-x_{2,t})q_{1,t}q_{2,t}\), and \(\Phi(x)=\sum_t[u_1a_{1,t}+u_2a_{2,t}+(u_{1,2}-u_1-u_2)b_t]\). Receiving neither message gives zero utility; repeated reception gives no additional utility.
Let \(D\) be the least common denominator of the masses and budget. For \(h=1/(Dn)\), start at zero and repeatedly add \(h\) to a feasible coordinate maximizing the exact increase in \(\Phi\), until total seed mass equals \(\beta\); permit every tie-breaking choice. Continuous greedy outcomes are all subsequential limits \((g,v)\) of terminal pairs \((g_h,\Phi(g_h))\) as \(n\to\infty\). Define \(\operatorname{OPT}(I)=\sup_{x\text{ feasible}}\Phi_I(x)\) and \(R=\inf_{I,(g,v)}v/\operatorname{OPT}(I)\), over the specified rational instances and their continuous greedy outcomes.

What is the exact worst-case ratio \(R\) of continuous marginal-gain greedy: is \(R=1/2\), or does it differ? Can instances of the specified mean-field influence model have limiting greedy ratios arbitrarily close to \(1/2\)?

For finite independent-cascade societies with disjoint seeds and these utility bounds, exact marginal-gain greedy guarantees \(1/2\); a discrete tightness result uses an abstract monotone bisubmodular function, without constructing an influence realization. [Sabato, Azaria and Hazon](https://www.ifaamas.org/Proceedings/aamas2020/pdfs/p1169.pdf)
Existing continuous influence maximization also studies discounts determining seed probabilities on finite graphs, a different problem. No result settling the specified mean-field ratio was located. [Continuous Influence Maximization](https://www.cs.sfu.ca/~jpei/publications/CIM%20SIGMOD16.pdf)

Modeling choices made when packaging the task

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

Result

The exact worst-case ratio is \(R=\frac12\). Moreover, acyclic instances with dyadic rational data have continuous greedy ratios tending to \(\frac12\).

The proof has two parts: a diminishing-returns argument establishing the lower bound for every permitted greedy outcome, and an explicit influence construction establishing tightness.

1. Diminishing returns for the specified cascade

Write \(e_{i,t}\) for the unit vector corresponding to message \(i\) and type \(t\). We first prove that \(\Phi\) is monotone and satisfies the following diminishing-returns property:

\[ \text{ } \]

For feasible allocations \(x\le y\) coordinatewise, and \(h\ge0\) such that \(y+h e_{i,t}\) is feasible,

\[ \Phi(x+h e_{i,t})-\Phi(x)\ \ge\ \Phi(y+h e_{i,t})-\Phi(y). \tag{1} \]

The argument uses finite-depth cascades, so it does not assume continuity of the limiting cascade at zero.

A branching-tree representation

At a vertex of type \(t\), independently generate, for each source type \(s\), a Poisson number of incoming children with mean \(\kappa_i(s,t)\mu_s\). Each child has type \(s\); recursively generate its incoming children in the same way.

Assign each vertex of type \(s\) an independent seed label in \(\{0,1,2\}\), with probabilities

\( \Pr(\text{label }i)=x_{i,s}/\mu_s,\qquad \Pr(\text{label }0)=1-(x_{1,s}+x_{2,s})/\mu_s. \)

In the tree for message \(i\), a vertex receives that message exactly when its subtree contains a vertex labelled \(i\).

For a root of type \(t\), the probability that its message-\(i\) tree contains an appropriately labelled nonroot vertex within depth \(r\) is \(q_{i,t}^{(r)}\). Indeed, a child of type \(s\) receives message \(i\) with probability

\( \frac{x_{i,s}}{\mu_s}+ \left(1-\frac{x_{i,s}}{\mu_s}\right)q_{i,s}^{(r)}. \)

Poisson thinning therefore gives exactly the recursion in the question.

For each root, take independent trees for the two messages, sharing only the root and its seed label. Conditional on that label, the two reception events are independent. Consequently, the expected utility at depth \(r\), multiplied by \(\mu_t\), is precisely the type-\(t\) contribution obtained by substituting \(q^{(r)}\) into the definitions of \(a\), \(b\), and \(\Phi\). Denote the resulting objective by \(\Phi_r\).

The trees can be coupled by truncating the same infinite trees. Reception events then increase with \(r\). The utility bounds imply that receiving an additional message never decreases utility. Hence

\[ \Phi_r(x)\uparrow\Phi(x). \tag{2} \]

Each \(\Phi_r\) is continuous, directly from the finite recursion.

Diminishing returns on a fixed finite tree

Fix a realization of the two depth-\(r\) trees. It has finitely many vertices almost surely. A partial seed assignment labels some vertices \(1\) or \(2\), leaving the others unassigned.

Let \(f\) be the root’s resulting utility. Consider adding label \(i\) at an unassigned vertex.

If this addition can activate message \(i\), its utility gain is one of

\( 0,\qquad u_i,\qquad u_{1,2}-u_j,\quad j\ne i. \)

The hypotheses give

\( 0\le u_{1,2}-u_j\le u_i. \)

Thus extending the existing assignment cannot increase the gain from assigning label \(i\) to an unassigned vertex: message \(i\) might already have arrived, and reception of the other message can only reduce its incremental utility. This also proves monotonicity of \(f\).

Let \(F(x)\) be the expected value of \(f\) under the independent categorical seed labels above. For a vertex \(v\) of type \(t\), let \(\Delta_{v,i}\) denote the gain from assigning label \(i\) when \(v\) is forced to be unassigned. Differentiating the finite product distribution gives

\[ \frac{\partial F}{\partial x_{i,t}} =\frac1{\mu_t}\sum_{v:\,\operatorname{type}(v)=t} \mathbb E[\Delta_{v,i}]. \tag{3} \]

For \(x\le y\), the categorical assignments at every other vertex can be coupled so that labels already present under \(x\) remain present under \(y\), while additional labels replace only unassigned states. Such a coupling exists because both label probabilities increase and their sum remains at most one.

The preceding diminishing-returns property of \(f\) therefore implies that every expectation in (3) is nonnegative and nonincreasing as \(x\) increases coordinatewise. Integrating (3) along the two feasible coordinate segments proves (1) for \(F\).

Averaging over the finite trees and root types proves monotonicity and (1) for \(\Phi_r\). Passing to the limit in (2) proves both properties for \(\Phi\). Also,

\[ \Phi(0)=0. \tag{4} \]

2. The universal lower bound

Fix a grid size \(h=1/(Dn)\). Replace each type \(t\) by \(\mu_t/h\) distinguishable atoms, each of mass \(h\). Assigning an atom one of the two messages corresponds to adding \(h\) to the appropriate coordinate. An atom can receive only one seed assignment.

Let \(f_h\) be \(\Phi\) evaluated at the resulting seed masses. Property (1) says that \(f_h\) has diminishing marginal gains under extension of a partial assignment. It is also monotone and vanishes at the empty assignment.

The budget permits exactly \(B=\beta/h\) assigned atoms. Coordinate greedy is equivalent to choosing an unassigned atom and label with maximum marginal gain.

Exchange proof of the grid guarantee

Let \(G_j\) be the greedy assignment after \(j\) steps. Let \(O_0\) be a grid optimum, extended to size \(B\) using monotonicity.

Maintain an assignment \(O_j\) of size \(B\) that extends \(G_j\). Suppose greedy next assigns atom \(e\) label \(i\).

In either removal case, call the removed atom-label pair \((a,k)\), and let \(O^{-}\) be the assignment after removal. Since \(O^{-}\) extends \(G_{j-1}\), diminishing returns gives

\( f_h(O_{j-1})-f_h(O^{-}) \le f_h(G_{j-1}+(a,k))-f_h(G_{j-1}). \)

The right-hand side is at most the greedy gain. Adding the greedy assignment to \(O^{-}\) cannot decrease its value. Thus, in every case,

\( f_h(O_{j-1})-f_h(O_j) \le f_h(G_j)-f_h(G_{j-1}). \)

At termination, \(O_B=G_B\). Summing and using (4) gives

\( f_h(O_0)-f_h(G_B)\le f_h(G_B), \)

so every grid-greedy terminal allocation satisfies

\[ \Phi(g_h)\ge\frac12\,\operatorname{OPT}_h. \tag{5} \]

Here \(\operatorname{OPT}_h\) is the grid optimum.

Passing to continuous outcomes

For any feasible \(x\), define its coordinatewise grid rounding by

\( x_{i,t}^{(n)}=h\left\lfloor x_{i,t}/h\right\rfloor. \)

It is feasible, lies below \(x\), and converges to \(x\). For every fixed \(r\), continuity of \(\Phi_r\) and the inequality \(\Phi\ge\Phi_r\) imply

\( \liminf_{n\to\infty}\Phi(x^{(n)})\ge\Phi_r(x). \)

Taking the supremum over \(r\), then using monotonicity for the reverse inequality, yields

\( \Phi(x^{(n)})\longrightarrow\Phi(x). \)

Consequently,

\[ \operatorname{OPT}_h\longrightarrow\operatorname{OPT}(I). \tag{6} \]

This argument requires neither attainment of the continuous optimum nor continuity of \(\Phi\).

For any subsequential terminal-pair limit \((g,v)\), (5) and (6) give

\[ v\ge\frac12\,\operatorname{OPT}(I). \tag{7} \]

The denominator is positive: seeding mass \(\beta\) with a message of maximum singleton utility gives utility at least \(\beta\max(u_1,u_2)>0\). Therefore (7) proves \(R\ge\frac12\).

3. An explicit rational influence family

Let \(J\ge4\) range over powers of two. Define

\( N=J^2,\qquad K=J^4,\qquad \rho=1-\frac1J. \)

Use the \(N+4\) types

\( A_1,\ldots,A_N,\ B,\ X,\ Y,\ Z, \)

with masses

\( \mu_{A_j}=\frac1{J^5},\qquad \mu_B=\frac1{J^3},\qquad \mu_X=\frac1J,\qquad \mu_Y=\frac12,\qquad \mu_Z=\frac12-\frac1J-\frac2{J^3}. \)

All masses are positive and sum to one. Set

\( \beta=\frac2{J^3},\qquad u_1=u_2=u_{1,2}=1. \)

Thus utility is the probability of receiving at least one message.

The only nonzero contact rates are

\( \kappa_1(A_j,X)=K,\qquad \kappa_1(B,X)=K, \)

and

\[ \kappa_2(A_j,Y)=r_j,\qquad r_j=\frac{2K}{J}\rho^j. \tag{8} \]

All data are dyadic rationals. The influence graph is acyclic: sources contact only \(X\) or \(Y\), which have no outgoing contacts.

For any allocation, put

\( z=\sum_{j=1}^{N}x_{1,A_j}+x_{1,B}, \qquad w=\sum_{j=1}^{N}r_jx_{2,A_j}, \qquad S=\sum_{i,t}x_{i,t}. \)

The cascade terminates after its first iteration, with

\( q_{1,X}=1-e^{-Kz},\qquad q_{2,Y}=1-e^{-w}, \)

and all other reception probabilities zero. Hence the objective is exactly

\[ \Phi(x)=S+ (\mu_X-x_{1,X}-x_{2,X})(1-e^{-Kz}) +(\mu_Y-x_{1,Y}-x_{2,Y})(1-e^{-w}). \tag{9} \]

4. A permissible greedy path on every grid

Choose ties so that greedy fills \(A_1,\ldots,A_N\), in that order, with message \(1\), then fills \(B\) with message \(1\).

We verify these choices using exact finite marginal gains.

The masses give \(D=J^5\), so every source capacity is an integer multiple of every prescribed grid size \(h=1/(J^5n)\).

Along the proposed path, \(w=0\), no target is seeded, and \(z\) is total seed mass. Adding \(h\) of message \(1\) to any available source has gain

\[ \Delta_1=h+\frac1J e^{-Kz}(1-e^{-Kh}). \tag{10} \]

These gains are identical across available sources.

Adding \(h\) of message \(2\) to an available \(A_\ell\) has gain

\[ \Delta_{2,\ell}=h+\frac12(1-e^{-r_\ell h}) \le h+\frac12 r_\ell h. \tag{11} \]

Every other available coordinate has gain at most \(h\), by (9).

While filling \(A_j\), all earlier source types are full and therefore unavailable for either message. Every available \(A_\ell\) has \(\ell\ge j\), and

\( K(z+h)\le K\sum_{\ell=1}^{j}\mu_{A_\ell}=\frac jJ. \)

Consequently,

\[ \frac1J e^{-Kz}(1-e^{-Kh}) =\frac1J\int_z^{z+h}Ke^{-Kt}\,dt \ge h\frac KJ e^{-j/J}. \tag{12} \]

On the other hand, \(\rho^\ell\le e^{-\ell/J}\), so (8) gives

\[ \frac12 r_\ell =\frac KJ\rho^\ell \le\frac KJ e^{-j/J}. \tag{13} \]

Equations (10)–(13) show that assigning message \(1\) to \(A_j\) maximizes the exact gain at every such step.

After all \(A_j\) are full, their message-\(2\) coordinates are blocked. Assigning message \(1\) to \(B\) has gain strictly greater than \(h\), while every other available coordinate has gain at most \(h\). Greedy therefore fills \(B\).

The terminal allocation is the same on every grid. It is thus a continuous greedy outcome, with value

\[ G_J=\frac2{J^3}+\frac1J(1-e^{-2J}). \tag{14} \]

5. A comparison allocation and the limiting ratio

Consider instead the feasible allocation assigning every \(A_j\) entirely message \(2\), and \(B\) entirely message \(1\). It also uses exactly \(\beta\).

Its message-\(1\) contact intensity into \(X\) is \(K\mu_B=J\). Its message-\(2\) contact intensity into \(Y\) is

\( \sum_{j=1}^{J^2}r_j\mu_{A_j} =\frac2{J^2}\sum_{j=1}^{J^2}\rho^j =\frac2J\,\rho(1-\rho^{J^2}). \)

Define \(C_J=\rho(1-\rho^{J^2})\). The comparison allocation has value

\[ H_J=\frac2{J^3} +\frac1J(1-e^{-J}) +\frac12\left(1-e^{-(2/J)C_J}\right). \tag{15} \]

Since \(\rho^{J^2}\le e^{-J}\), we have \(C_J\to1\). Equations (14) and (15) therefore give

\( JG_J=\frac2{J^2}+1-e^{-2J}\longrightarrow1, \)

and, using \((1-e^{-a})/a\to1\) as \(a\to0\),

\( JH_J=\frac2{J^2}+1-e^{-J} +\frac J2\left(1-e^{-(2/J)C_J}\right) \longrightarrow2. \)

We do not need to identify the actual optimum: feasibility gives \(\operatorname{OPT}(I_J)\ge H_J\), while the universal bound (7) gives

\( \frac12\le \frac{G_J}{\operatorname{OPT}(I_J)} \le\frac{G_J}{H_J} \longrightarrow\frac12. \)

Thus the actual limiting greedy ratios of this rational, acyclic family approach \(\frac12\). Together with the universal lower bound, this settles both questions.

⟨structured verdict parsed — rendered above⟩

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

Verdict

The proof establishes \(R=\frac12\) and constructs admissible instances whose continuous greedy ratios approach \(\frac12\). Both the universal lower bound and the tightness construction are rigorous. I found no major or minor issue requiring clarification.

Step-by-step verification

1. Branching-tree representation

The proposed representation matches the specified recursion. For a message-\(i\) child of type \(s\), activation has probability \(x_{i,s}/\mu_s+(1-x_{i,s}/\mu_s)q_{i,s}^{(r)}\). Multiplying by its Poisson mean \(\kappa_i(s,t)\mu_s\) gives precisely the contribution \(\kappa_i(s,t)(x_{i,s}+(\mu_s-x_{i,s})q_{i,s}^{(r)})\) to the next iteration.

The use of independent message trees with a shared root seed label correctly reproduces the stipulated conditional independence. In particular, the root’s joint reception probability is the stated \(b_t\).

Every finite-depth tree has finitely many vertices almost surely: there are finitely many types, all contact rates are finite, and every vertex has finitely many Poisson children almost surely.

The utility assumptions ensure that reception of an additional message never lowers utility. Thus truncations of the same trees give \(\Phi_r(x)\uparrow\Phi(x)\). Continuity of each \(\Phi_r\) follows from its finite recursion.

This argument respects least-fixed-point selection and does not assume continuity of the limiting cascade.

2. Monotonicity and diminishing returns

On a fixed finite tree, a relevant addition of label \(i\) has gain \(u_i\) when only that message becomes available, and gain \(u_{1,2}-u_j\) when the other message is already available. If it does not newly activate message \(i\), its gain is zero.

The bounds \(0\le u_{1,2}-u_j\le u_i\) follow from the task’s utility assumptions. Extending an assignment can therefore only preserve or reduce the gain of an additional label. This verifies the fixed-tree monotonicity and diminishing-returns assertions, including the shared root.

Equation (3) correctly differentiates the categorical product distribution. Increasing \(x_{i,t}\) increases the probability of label \(i\) and decreases the probability of the unassigned state by the same amount, while leaving the other label probability unchanged. Summing the resulting contributions over vertices of type \(t\) accounts for all occurrences of that parameter.

For \(x\le y\), the claimed coupling exists: retain every existing nonzero label and distribute the additional label probabilities among previously unassigned states. Feasibility guarantees sufficient unassigned probability.

Integrating the derivative inequality proves (1) on each fixed tree. Averaging preserves the inequality. Passing to the finite-depth limit also preserves it, since all objective values converge and are bounded.

Finally, \(\Phi(0)=0\) is correct: every iterate of the prescribed recursion is zero at zero seeds, even if other fixed points exist.

3. Grid exchange argument

The atom construction is valid because \(\mu_t/h\) and \(B=\beta/h\) are integers. Assignments of atoms yield exactly the feasible grid allocations.

The objective depends only on the aggregate seed masses, so choosing an available atom-label pair with maximum marginal gain is equivalent to the coordinate greedy rule.

All three exchange cases preserve the required invariant: \(O_j\) has size \(B\) and extends \(G_j\). In either removal case, the removed pair lies outside \(G_{j-1}\), so adding it to \(G_{j-1}\) is feasible. Moreover, \(O^{-}\) extends \(G_{j-1}\), and restoring the removed pair to \(O^{-}\) is feasible. These facts verify the hypotheses needed for the diminishing-returns comparison.

Greedy maximality bounds the removal loss by the greedy gain, and monotonicity permits the subsequent addition. At termination, the equal-size extension forces \(O_B=G_B\). The telescoping calculation therefore proves (5) for every tie-breaking choice.

4. Passage to continuous outcomes

Coordinatewise rounding remains feasible and converges to the original allocation. For every fixed depth, continuity gives the asserted lower bound on the limit inferior. Taking the supremum over depths recovers \(\Phi(x)\), while monotonicity supplies the upper bound.

Consequently, rounded values converge even when \(\Phi\) itself is discontinuous.

Equation (6) follows without requiring attainment of the continuous optimum: grid optima are bounded above by the continuous supremum, and the rounding argument applies to every feasible allocation.

Passing (5) along any convergent terminal-pair subsequence proves (7) for its value coordinate \(v\). The argument correctly does not require \(v=\Phi(g)\).

The denominator is positive because the utility assumptions give \(\max(u_1,u_2)>0\), and a feasible allocation can seed mass \(\beta\) with that message. Thus the universal ratio bound is well-defined.

5. Admissibility and objective of the construction

The source masses total \(2/J^3\), and the displayed masses sum to one. The smallest permitted \(J\), namely \(J=4\), already gives positive \(\mu_Z\). The budget and utilities satisfy every required restriction.

For powers of two \(J\), all masses, the budget, and the rates \(r_j\) are dyadic rationals. Also, \(D=J^5\): this denominator accommodates all masses and the budget, and an \(A_j\) mass requires it.

The only positive contact rates lead from uncontacted source types into terminal types \(X\) and \(Y\). Consequently, the displayed reception probabilities are exact after the first iteration.

Equation (9) correctly counts certain seed utility plus reception by unseeded target mass. With utility one for receiving either or both messages, seeded target individuals contribute no further utility through reception.

6. Exact greedy-path verification

Equation (10) is the exact message-\(1\) source marginal. Equation (11) is the exact message-\(2\) source marginal followed by the valid bound \(1-e^{-a}\le a\).

While filling \(A_j\), the endpoint bound \(K(z+h)\le j/J\) holds on every prescribed grid. It yields (12), including its constant \(K/J\).

The inequality \(\rho^\ell\le e^{-\ell/J}\), together with \(\ell\ge j\), gives (13). Thus the proposed message-\(1\) choice has at least as large an exact gain as every available message-\(2\) source choice. Other message-\(1\) sources tie, as permitted.

Every remaining coordinate has gain at most \(h\). Once the \(A_j\) types are full, their competing labels are unavailable, and message \(1\) at \(B\) has gain strictly greater than \(h\). This verifies the entire proposed path.

Its allocation is identical on every grid, so its terminal pair is indeed a continuous greedy outcome. Equation (14) correctly uses \(Kz=2J\).

7. Tightness calculation

The comparison allocation is feasible and uses exactly the budget. Its two contact intensities are correctly calculated as \(J\) and \((2/J)\rho(1-\rho^{J^2})\). The geometric sum and equation (15) are correct.

The estimate \(\rho^{J^2}\le e^{-J}\) proves \(C_J\to1\). The subsequent limits give \(JG_J\to1\) and \(JH_J\to2\), hence \(G_J/H_J\to\frac12\).

Feasibility supplies the upper comparison with the actual optimum, while the already-proved universal guarantee supplies the lower comparison. The squeeze argument therefore establishes convergence of the actual greedy ratios to \(\frac12\), rather than merely convergence relative to a comparison allocation.

No repair or additional clarification is needed. The result establishes an exact approximation ratio; it makes no polynomial-time claim about exact marginal evaluation.

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