Optimal Auctions beyond Independent Private Values Exact robust design in semialgebraic finite games

\section*{Optimal Auctions beyond Independent Private Values\\[4pt]
 \large Exact robust design in semialgebraic finite games}

Ji Ho Bae\\\small LawAll AI 10 October 2026 \begin{center} \small\textbf{D44-34 \quad JEL D44 \quad Source OP-0007} \end{center} \begin{abstract} We give an exact algorithmic theorem for the entire specified rational-semialgebraic design continuum of finite perfect-recall auctions. Correlation, interdependence, monetary risk, private liquidity, and endogenous entry and information acquisition are retained. A fixed-game polynomial Bayes-graph closure encodes genuine sequential equilibrium, with full continuation rationality and nonempty compact assessment fibers. Classical real quantifier elimination then computes the robust value against all environments and all sequential equilibria, decides attainment, and constructs same-class algebraic $\varepsilon$-mechanisms. We also characterize actual achievable guarantees in a specified simpler format, including unattained threshold cases. The complexity statement is polynomial in input bit precision only when all compiled variable and degree bounds are fixed. A nonlinear example has strictly active costly acquisition and a $1/16$ guarantee against the same budget-feasible class. The algorithm is proved; a full all-friction CAD execution is not claimed. \end{abstract} \section{The declared design continuum and information structure}\label{wsref-0-73-65-63-3a-6d-6f-64-65-6c} The canonical question permits a stated environment collection and feasible mechanism class. Here the input specifies finitely many finite perfect-recall auction formats. A format records Nature's finite type and payoff-state draws, each bidder's information partition, entry, acquisition, report, bid and exit choices, physical outcomes, and a seller-observable-history partition. Mechanism parameters $m$ range over the entire specified semialgebraic domain $D$, and environment parameters $\omega$ over a specified semialgebraic set $\Omega$. The initial nonemptiness tests below handle empty sets explicitly. Compactness is not assumed. All input formulas have rational coefficients. Algebraic constants may instead be specified by polynomials and isolating intervals. Primitive Nature probabilities, values, budgets, costs, participation benchmarks, and utility functions have finite semialgebraic graph descriptions. Each graph must define a total, single-valued, finite-valued function on its admitted domain. An arbitrary relation, a missing graph point, or an undefined $0/0$ is not a valid primitive. The class includes piecewise rational and algebraic functions; it does not include arbitrary unrepresented utility functions. Graph variables replace function notation when formulas are compiled. The designer chooses $m$ before the environment is selected. At each fixed $\omega$, the probabilistic and payoff specification is common knowledge among bidders, while realized private signals and liquidity remain private. Seller-controlled transfers, allocations, and randomization depend only on $m$, the seller's actual observations, and its own random draws. They coincide on seller-indistinguishable histories and cannot depend on hidden Nature labels or unobserved $\omega$. Exogenous type and acquisition kernels may depend on the environment and hidden states as specified by the experiment. Monetary utility is nondecreasing on its declared monetary domain. Its values are applied to the realized terminal monetary argument before expectation. Terminal-utility graphs must be the specified compositions of values, transfers, monetary utility, and costs. Quasilinearity is not assumed. Cash entry or acquisition costs belong in terminal monetary wealth and in the cash account at their actual dates. Nonmonetary disutilities, when declared, are subtracted outside monetary utility; these conventions cannot be interchanged. Seller-directed charges are included in seller payments, while payments to outside parties are not seller revenue. Realized allocations $x_z$ belong to the finite feasible allocation set $X$. A finite lottery is represented by its Nature draw before the terminal leaves. With finite-valued seller cost $C:X\to\mathbb R$, terminal seller profit is \begin{equation}\label{wsref-0-65-71-3a-73-65-6c-6c-65-72-6c-65-61-66} r_z(m)=\sum_i\tau_{i,z}(m)-C(x_z). \end{equation} It has no direct dependence on hidden $\omega$; the environment can change which terminal history occurs. The construction below is uniform in arbitrary finite input templates. A finite input collection is a tagged finite union. It does not turn an unspecified unbounded union of all finite trees into one fixed finite-dimensional optimization problem. \section{Legal games, true cash, and uniform input validity}\label{wsref-0-73-65-63-3a-76-61-6c-69-64-69-74-79} Private-budget action availability, when present, is part of the actual game family. A semialgebraic legality guard is identical at all nodes of the acting bidder's information set. Every live decision has an available action. Split the parameter domain into its finitely many legality-guard patterns before considering Nature support. Each pattern determines a legal tree with its information partition; perfect recall is checked there. The pattern is determined by $(m,\omega)$, not chosen by a seller who does not know the environment. An available action remains in the game even if its equilibrium probability is zero. The hard-liquidity convention concerns actual feasible expenditure. Every prefix of every Nature-supported legal history must leave nonnegative cash, starting from the true budget $b_i(\omega,s_i)$. Actual deposits and cash payments are debited when made; refunds are credited when received. A later refund cannot finance an earlier unaffordable escrow deposit. For the standard initial-budget account, cumulative net seller payments plus declared nonnegative outside cash costs cannot exceed that budget. In particular this account is required to imply, at every legal terminal, \[ \tau_{i,z}(m)+k_{i,z}^{\mathrm{outside}}(m,\omega) \le b_i(\omega,s_i(z)),\qquad k_{i,z}^{\mathrm{outside}}\ge0. \] Thus net seller payments themselves are bounded by the true budget. False reports do not create cash or enlarge physically feasible moves. Affordability-based menus are compatible with private liquidity when the player knows and remembers its own cash; an actual deposit implements the restriction without revealing the true budget to the seller.

These tests apply at every structurally live legal history, including histories reached with zero probability in a proposed equilibrium. They are not multiplied by equilibrium reach probabilities. Testing payments only at an equilibrium cannot repair an incorrect deviation set. Every legal deviation and every completely mixed legal perturbation must already be physically feasible. Alternative funding or account conventions require their own explicitly proved terminal-payment upper envelope in the value argument below. Terminal netting must not erase intermediate cash requirements.

Totality and functionality of graphs, proper Nature probabilities, nonempty legal action sets, perfect recall, observation restrictions, and monotonic monetary utility are uniform input hypotheses or explicitly tested predicates. For example, functionality means that two graph values at the same argument are equal; totality is existence of a value at every admitted argument. Both are first-order real conditions. Nondecreasing utility is tested on its declared domain by the corresponding two-argument implication. An invalid graph or game cannot be hidden in a false antecedent that makes an adverse environment disappear.

Participation is separately declared as ex ante or interim and is required at every admitted equilibrium. For positive-probability interim participation, a division-free form is \begin{equation}\label{wsref-0-65-71-3a-69-6e-74-65-72-69-6d-49-52} \sum_{z:s_i(z)=s_i}\Pr(z)\,u_{i,z} \ge \Pr(s_i)\,u_i^{\mathrm{out}}(\omega,s_i). \end{equation} Here $u_{i,z}$ is actual terminal utility, and probabilities use the true signal law. At a zero-marginal signal this expresses the declared vacuous convention. Any additional condition at such a signal must be specified separately; no posterior is invented for a null type. Ex-post participation is a different restriction and is not substituted.

The proof constructs the formulas and verifies their meanings in Sections sec:bayes--sec:simple; it invokes a complete classical real quantifier-elimination algorithm. No execution of that full CAD computation is claimed.

Nature support and exact Bayes polynomials

Work first with one fixed legal tree. Perfect recall means that all nodes in one bidder information set have the same sequence of that bidder's preceding information sets and actions. In particular an information set is never revisited along a path. Let $p=(m,\omega)$. Lift Nature probabilities and terminal utilities to vectors $c,u$, with a supplied graph predicate $\operatorname{Graph}(p,c,u)$. They are uniquely determined by $p$. Rational functions use nonzero-denominator guards and multiplication equations; an undefined conditional $0/0$ must first be completed semialgebraically or replaced by an unconditional signal draw. The vectors $c,u$ are fixed outside every tremble quantifier.

For each subset $S$ of Nature edges, impose \[ c_e>0\quad(e\in S),\qquad c_e=0\quad(e\notin S), \] together with nonnegativity and unit outgoing sums at every Nature node. These finitely many strata include boundary cases; empty ones may be discarded. At fixed $p$, exactly one support pattern applies. A history is Nature-live when every Nature factor in its prefix is positive. Remove only the other histories. At a surviving Nature node retain the original positive probabilities, which still sum to one. At a surviving strategic node retain all its legal actions. A strategic edge cannot introduce a zero Nature factor, and each successor has a live terminal continuation by finiteness and the unit sums.

Replace information set $I$ by its live intersection $I^S$, omitting it only if empty. Its available actions are unchanged. Every prefix of a live history is live, so remembered own information and actions are unchanged and perfect recall is preserved. Assessments below refer to this actual-support game. Strategically off-path legal histories remain. An entirely Nature-impossible information set has Bayes denominator zero under every strategic tremble; imposing ordinary Bayes beliefs there while asserting nonemptiness would be inconsistent. Assigning arbitrary such beliefs is an extra convention, not fixed-Nature consistency. The explicit support convention removes that ambiguity. The actual-support game is a finite perfect-recall game in which every remaining Nature action has positive probability, wherever its Nature node lies in the tree. This is the requirement on chance moves in Bonanno's definition of a finite extensive form, in which chance may move at any history [Bonanno2015] (Appendix 12.A, p. 443); his Definition 11.1 $p.~391$ defines consistency for such games.

On a stratum, let $\mathcal I_S$ be the retained strategic information sets, and write \begin{align*} \mathsf B_S(\sigma):\quad& \sigma_{I,a}\ge0,\quad\sum_{a\in A(I)}\sigma_{I,a}=1 &&(I\in\mathcal I_S),\\ \mathsf B_S^+(\sigma):\quad& \mathsf B_S(\sigma),\quad \sigma_{I,a}>0 &&(I\in\mathcal I_S,\ a\in A(I)),\\ \mathsf M_S(\mu):\quad& \mu_{I,h}\ge0,\quad\sum_{h\in I^S}\mu_{I,h}=1 &&(I\in\mathcal I_S). \end{align*} Define the reach polynomial $P_h(c,\sigma)$ as the product of the probabilities along the root-to-$h$ path, using $c$ on Nature edges and $\sigma_{I,a}$ on strategic edges, with $P_{\mathrm{root}}=1$. Equivalently generate them recursively down the tree. Set $P_I=\sum_{h\in I^S}P_h$. Every retained history, and hence every $I$, has positive reach under $\mathsf B_S^+$. The exact Bayes graph is \begin{equation}\label{wsref-0-65-71-3a-42-61-79-65-73} \begin{split} \operatorname{BG}_S(c,\sigma,\mu):={}& \mathsf B_S^+(\sigma)\wedge\mathsf M_S(\mu)\\ &{}\wedge\bigwedge_{I\in\mathcal I_S} \left[P_I(c,\sigma)>0\ \wedge\ \bigwedge_{h\in I^S}\mu_{I,h}P_I(c,\sigma)=P_h(c,\sigma)\right]. \end{split} \end{equation} The positive-denominator guards prevent a cross-multiplied $0=0$ from admitting spurious beliefs. Each completely mixed strategic profile has exactly one Bayes belief vector. In bookkeeping with original partially live sets, removed nodes have belief zero. Empty sets have no assessment coordinates. Different strata form a tagged finite disjoint union; common-dimensional padding may use fixed dummy zeros, which are not beliefs at existing sets.

Full continuation rationality

Fix player $i$, its information set $I$, and a behavioral continuation $\delta_i$ in the product $\Delta_i$ of its retained action simplexes. Components preceding $I$ or never encountered later are irrelevant. For $h\in I^S$ and terminal descendant $z$, let $T^i_{h,z}(c,\sigma_{-i},\delta_i)$ be the product along the suffix from $h$ to $z$: Nature uses $c$, other players use $\sigma$, and $i$ uses $\delta_i$. Set it to zero if $z$ is not descended from $h$. The exact conditional continuation payoff is the polynomial \begin{equation}\label{wsref-0-65-71-3a-63-6f-6e-74-69-6e-75-61-74-69-6f-6e} V_{i,I}(c,u,\sigma_{-i},\delta_i;\mu) =\sum_{h\in I^S}\mu_{I,h} \sum_{z\text{ descended from }h} u_{i,z}\,T^i_{h,z}(c,\sigma_{-i},\delta_i). \end{equation} There is no zero-probability conditioning: $\mu_I$ is an explicit part of the assessment and is fixed for this comparison. All entry and information-acquisition choices in the tree are included.

Define $\operatorname{SR}_S(c,u,\sigma,\mu)$ by requiring, for every $i,I$, \begin{equation}\label{wsref-0-65-71-3a-53-52} \forall\delta_i\left[ \delta_i\in\Delta_i\ \Longrightarrow\ V_{i,I}(c,u,\sigma_{-i},\sigma_i;\mu) \ge V_{i,I}(c,u,\sigma_{-i},\delta_i;\mu)\right]. \end{equation} This is optimality of the entire continuation at every information set. Other bidders' behavior is fixed, not their hypothetical responses to the deviation. Neither beliefs nor admissible actions are replaced.

The number of inequalities may be exponential, but it is finite and constructible. No one-step-deviation or PBE replacement is used. Without perfect recall, repeated visits can destroy block affinity; that extension is not claimed.

Consistency at a fixed game and the exact equilibrium predicate

We use finite-game consistency in the sense of Kreps--Wilson [KW1982]. For assessments define \[ d^2((\sigma,\mu),(\sigma',\mu')) =\sum_{I,a}(\sigma_{I,a}-\sigma'_{I,a})^2 +\sum_{I,h}(\mu_{I,h}-\mu'_{I,h})^2. \] The exact consistency condition is the following first-order formula: \begin{equation}\label{wsref-0-65-71-3a-63-6f-6e-73-69-73-74-65-6e-63-79} \operatorname{Con}_S(c,\sigma,\mu):= \forall r\left[ r\le0\ \vee\ \exists\sigma',\mu'\left( \operatorname{BG}_S(c,\sigma',\mu')\ \wedge\ d^2((\sigma,\mu),(\sigma',\mu'))<r^2\right)\right]. \end{equation} The same fixed $c$ occurs throughout. Mechanism $m$, environment $\omega$, and Nature probabilities do not vary. One common $\sigma'$ and its complete Bayes vector $\mu'$ must satisfy all information-set equations simultaneously. No rationality or equilibrium condition is imposed on this witness. No lower bound ties its action probabilities to $r$; different trembles may vanish at arbitrary relative rates. Thus consistency is the closure of one fixed-$c$ Bayes graph in the finite-dimensional assessment space, not a closure across environments or separately for different information sets.

On each legal support stratum define \begin{equation}\label{wsref-0-65-71-3a-53-45} \begin{split} \operatorname{SE}_S(p,\sigma,\mu):={}&\mathcal P(p)\ \wedge\ \exists c,u\bigl[ \operatorname{Graph}(p,c,u)\wedge\operatorname{ValidChance}(c) \wedge\operatorname{Supp}_S(c)\\ &{}\wedge\mathsf B_S(\sigma)\wedge\mathsf M_S(\mu) \wedge\operatorname{SR}_S(c,u,\sigma,\mu)\wedge\operatorname{Con}_S(c,\sigma,\mu) \bigr]. \end{split} \end{equation} Here $\mathcal P$ includes the stratum's fixed legality conditions. The graph vector is quantified outside the tremble condition. Taking a tagged finite disjunction, with the dummy-coordinate convention above when necessary, gives $\operatorname{SE}(p,e)$, $e=(\sigma,\mu)$. A parameter $p$ is admitted for the stratum $S$ when the primitive graphs are total and single-valued at $p$, $\mathcal P(p)$ holds, its Nature vector $c$ is proper and satisfies $\operatorname{Supp}_S(c)$, every live decision has an available legal action, and its legal tree has perfect recall (Section sec:validity). The legal actual-support game of an admitted parameter is called valid.

Parameters kept free are variable values, not unencoded irrational coefficients in the algorithmic input. For individual rational or real-algebraic parameters, exact numerical encodings give equilibrium descriptions and algebraic sample assessments. No finite algorithm for arbitrary unencoded real constants is asserted. If a primitive graph is initially given by a first-order rational formula, eliminate its quantifiers first; its totality and functionality still must hold. Graf, Engesser, and Nebel [GEN2024], Definition 3 and Sections 3.1--3.2, already develop exact polynomial representations of sequential equilibrium.

Nonempty compact equilibrium fibers

The special positive profiles in this existence proof are constrained agent-game equilibria. They are not an extra restriction on the witnesses in (eq:consistency), which remain arbitrary completely mixed profiles. Compactness is a statement about each fixed game. It implies neither a closed joint graph nor continuity across Nature-support changes or discontinuous primitive graphs.

Three exact consistency diagnostics

Arbitrary off-path beliefs can fail

Players 1 and 2 simultaneously choose Out or In, receiving $0$ for Out and $-1$ for In regardless of subsequent play. If someone enters, player 3 moves without seeing who entered. Its information set has nodes Both, Only1, and Only2. Action $L$ pays it $1$ at Both and $0$ otherwise; action $R$ pays $0$ at Both and $1$ otherwise. This has a finite perfect-recall representation. Both early players strictly choose Out. On-path Bayes equations alone permit belief one on Both and choice $L$, which is then a best reply. It is not sequentially consistent. For completely mixed entry probabilities $p,q$, \[ \mu(\mathrm{Both}) =\frac{pq}{pq+p(1-q)+(1-p)q} =\frac{pq}{p+q-pq}\le\min\{p,q\}. \] As $p,q\to0$, consistency forces belief zero on Both. Every sequential equilibrium therefore prescribes $R$. Removing the strategically off-path information set would lose this restriction.

Different information sets need a common witness

Let player 1 choose Out, $L$, or $R$, with Out terminal. After $L$ or $R$, player 2 has an information set $I$ with a forced action, then an information set $J$, still unable to distinguish $L$ from $R$. Perfect recall holds; payoffs may all be zero. Every completely mixed profile gives the same $L/R$ posterior at both sets. When the limiting strategy chooses Out with probability one, either posterior separately can approach any value, but their limits must coincide. Independent information-set witnesses would wrongly permit $\mu_I(L)=1$, $\mu_J(L)=0$.

Varying the parameter in the closure perturbs Nature

Nature chooses $A$ with probability $p$, and $B$ otherwise. Player 1 observes the state and chooses Enter or Out; after entry player 2 cannot distinguish the states. For $0<p<1$, use entry probabilities $1/2$ at $A$ and $p^2$ at $B$, completed to fully mixed profiles. The entry posterior of $A$ is \[ \frac{p/2}{p/2+(1-p)p^2}\longrightarrow1\quad(p\downarrow0). \] At fixed $p=0$, state $A$ is Nature-impossible. Entry at $B$ is live, even if the limiting strategic probability is zero, and strategic trembles force its posterior to be $B$ with probability one. Closing over varying parameters gives the wrong assessment; (eq:consistency) keeps this game fixed.

Robust feasibility and the inner worst equilibrium

Let $e=(\sigma,\mu)$, and let $\operatorname{SE}(m,\omega,e)$ be the exact finite-disjunction formula above. The expected seller profit is \begin{equation}\label{wsref-0-65-71-3a-72-65-76-65-6e-75-65} \operatorname{Rev}(m,\omega,e)=\sum_z P_z(c,\sigma)\,r_z(m). \end{equation} Beliefs constrain equilibria but do not replace actual path probabilities in this expression. After primitive graphs are lifted, it is semialgebraic. At fixed parameters it is a continuous polynomial in behavior. In (eq:revenue), $c$ is the Nature vector of $p=(m,\omega)$ given by $\operatorname{Graph}(p,c,u)$, and $z$ ranges over the terminal set $Z_S$ of the legal actual-support game of the stratum $S$ containing $p$. In formulas an atom $\operatorname{Rev}(m,\omega,e)\bowtie v$, with $\bowtie$ one of $=$ and $\ge$, stands for the disjunction over strata $S$ of \[ \mathcal P(p)\wedge\exists c,u\left[\operatorname{Graph}(p,c,u)\wedge \operatorname{Supp}_S(c)\wedge \sum_{z\in Z_S}P_z(c,\sigma)\,r_z(m)\bowtie v\right]. \] Thus $c$ and $u$ are bound in (eq:worstfixed), (eq:guarantee), and all later formulas. Where the graphs are total and single-valued, exactly one stratum and one graph vector qualify, so the atom compares $v$ with (eq:revenue) at the actual Nature vector. Theorem Theorem (Fixed-game existence and compactness) makes the inner worst-equilibrium value an attained minimum. Its value relation is exactly \begin{equation}\label{wsref-0-65-71-3a-77-6f-72-73-74-66-69-78-65-64} \begin{split} \operatorname{Worst}(m,\omega,v):={}& \exists e\,[\operatorname{SE}(m,\omega,e)\wedge\operatorname{Rev}(m,\omega,e)=v]\\ &{}\wedge \forall e'\,[\operatorname{SE}(m,\omega,e')\Rightarrow \operatorname{Rev}(m,\omega,e')\ge v]. \end{split} \end{equation} In particular the universal clause includes unfavorable equilibria.

Write $\mathcal F(m)$ for robust feasibility. It includes $D(m)$, uniform graph and game validity under every $\omega\in\Omega$, physical allocation and true-prefix-cash constraints from Section sec:validity, and the declared participation inequalities for every $\omega$ and every $e$ satisfying $\operatorname{SE}(m,\omega,e)$. One may retain the redundant explicit check $\exists e\,\operatorname{SE}(m,\omega,e)$. It is proved true for every valid game.

All parts are finite first-order formulas. Graph totality and uniqueness, probability constraints, legal-action guards, observation equalities, and utility monotonicity are uniformly verified hypotheses or quantified predicates. The finite combinatorial recall tests are performed on the legal templates. The remaining budget and allocation tests are imposed on every structurally live legal history. The participation conditions include the true-probability version of (eq:interimIR) or the declared ex-ante alternative. In (eq:interimIR), $\Pr(z)=P_z(c,\sigma)$ and $\Pr(s_i)=\sum_{z\in Z_S:\,s_i(z)=s_i}P_z(c,\sigma)$, with $c$ and $u$ bound as in the revenue atoms. These predicates and their universal quantifiers are passed to the same complete algebraic procedure.

The robust order is one design choice before all environments and all equilibria: \[ \exists m\quad\forall\omega\in\Omega\quad \forall e\in\mathcal E(m,\omega). \] Validity is required separately for every environment. It cannot be hidden solely in an equilibrium implication with a false antecedent. Legality and support patterns are functions of the actual parameters, not extra favorable choices for the designer. First decide whether $\Omega$ and $\{m:\mathcal F(m)\}$ are nonempty. If either is empty, report that fact and no optimizer.

A finite robust value without compactness assumptions

Assume the environment and feasible design sets are nonempty. For each feasible mechanism define \[ W(m)=\inf_{\omega\in\Omega}\inf_{e:\operatorname{SE}(m,\omega,e)} \operatorname{Rev}(m,\omega,e). \] No minimum over environments or maximum over mechanisms is presumed. For fixed $m$, its finitely many finite terminal seller profits are independent of hidden $\omega$. Therefore \begin{equation}\label{wsref-0-65-71-3a-6c-65-61-66-62-6f-75-6e-64-73} \min_z r_z(m)\le\operatorname{Rev}(m,\omega,e)\le\max_z r_z(m) \end{equation} for every environment and equilibrium. In particular $W(m)$ is finite even when $\Omega$ is not compact.

Exact real-algebraic sample-point extraction, detailed below, gives an algebraic feasible $m_0$ and an algebraic $\omega_0\in\Omega$. The first point is extracted from the actual quantified feasibility condition $\mathcal F$, not merely from $D$. Set \[ L_0=\min_z r_z(m_0). \] Then $V^*=\sup_{\mathcal F(m)}W(m)\ge W(m_0)\ge L_0$. At the fixed environment $\omega_0$, true terminal cash feasibility for every feasible mechanism gives \[ \sum_i\tau_i\le\sum_i\max_{s_i}b_i(\omega_0,s_i). \] Nonnegative external cash costs only reduce the cash available for seller payments. Hence \begin{equation}\label{wsref-0-65-71-3a-76-61-6c-75-65-62-6f-75-6e-64} V^*\le B_0:= \sum_i\max_{s_i}b_i(\omega_0,s_i)-\min_{x\in X}C(x)<\infty. \end{equation} Indeed every equilibrium at $\omega_0$ satisfies this pointwise upper bound, and the infimum over all environments is no larger. For an alternative funding convention the same argument is used only when its own finite, effectively specified uniform seller-profit envelope has been supplied and proved. Unbounded external funding is not included in the finite-value claim. Thus $V^*$ is a finite real number by explicit cash bounds, without equilibrium continuity or strict-obedience assumptions.

Exact value, attainment, and same-class approximations

Define the lower-guarantee predicates \begin{align} A(m,t)&:=\mathcal F(m)\ \wedge\ \forall\omega,e\, [\,\Omega(\omega)\wedge\operatorname{SE}(m,\omega,e) \Rightarrow\operatorname{Rev}(m,\omega,e)\ge t\,],\label{wsref-0-65-71-3a-67-75-61-72-61-6e-74-65-65}\\ B(t)&:=\exists m\,A(m,t).\label{wsref-0-65-71-3a-74-68-72-65-73-68-6f-6c-64} \end{align} Because all equilibrium fibers are nonempty, $A(m,t)$ means precisely $\mathcal F(m)$ and $W(m)\ge t$, whether or not the inner environment infimum is attained. The truth set of $B$ is nonempty, downward closed, and has finite supremum $V^*$. Define \begin{equation}\label{wsref-0-65-71-3a-56-61-6c-75-65} \begin{split} \operatorname{Value}(v):={}& [\,\forall t\ (B(t)\Rightarrow t\le v)\,]\\ &{}\wedge [\,\forall\eta>0\ \exists t\ (B(t)\wedge t>v-\eta)\,]. \end{split} \end{equation} These are real quantifiers; positivity is an ordinary polynomial guard. This explains the extraction used in Section sec:bounds. All statements invoke a complete classical algebraic algorithm with the hypotheses verified in Theorem Theorem (Exact symbolic assessment set).

Exact attainment is decided by \begin{equation}\label{wsref-0-65-71-3a-61-74-74-61-69-6e-6d-65-6e-74} \exists m\,A(m,V^*). \end{equation} If true, Lemma Lemma (Exact sample witnesses) extracts an algebraic optimizer. If false, the correct report is nonattainment. For every rational $\varepsilon>0$, \begin{equation}\label{wsref-0-65-71-3a-65-70-73-69-6c-6f-6e} \exists m\,A(m,V^*-\varepsilon) \end{equation} is true by the definition of supremum and downward closure. Extracting a point gives a mechanism in the original feasible class satisfying \[ \inf_{\omega\in\Omega}\inf_{e\in\mathcal E(m_\varepsilon,\omega)} \operatorname{Rev}(m_\varepsilon,\omega,e)\ge V^*-\varepsilon. \] For any real $\varepsilon>0$, existence follows by choosing a smaller positive rational tolerance. Exact algebraic coordinate names are the output convention. Rational or decimal rounding is not part of this guarantee: it may change tie incentives or violate an equality constraint. No truthful-report revelation principle, equilibrium selection, discretization continuity, or uniform strict-incentive margin is used.

A rational-interval certificate alternative

Exact value extraction is unnecessary for a requested approximation. Choose rational $L\le L_0$ and $U\ge B_0$, and keep the witness $A(m_0,L)$. Query $B((L+U)/2)$. If true, extract a witness and replace $L$ by the midpoint. If false, replace $U$ by it: downward closure implies $V^*\le U$, even when the supremum is unattained. For positive initial width, after at most \begin{equation}\label{wsref-0-65-71-3a-62-69-73-65-63-74-69-6f-6e} \max\left\{0, \left\lceil\log_2\frac{U_{\mathrm{initial}}-L_{\mathrm{initial}}} {\varepsilon}\right\rceil\right\} \end{equation} steps, $U-L\le\varepsilon$. Handle zero initial width separately with no queries. The saved lower witness satisfies \[ L\le W(\widehat m)\le V^*\le U. \] Every query is decided by the same complete real-algebraic algorithm. A checkable output contains the compiled formulas, exact mechanism coordinates, certificates for $A(\widehat m,L)$, the false threshold decisions actually used, and the initial cash upper bound. With exact $V^*$, one can instead certify $A(\widehat m,V^*-\varepsilon)$ directly.

Simpler formats, nonattainment, and threshold equality

Let $S$ be a declared semialgebraic subformat of the same design domain, inheriting the same environments, constraints, and equilibrium correspondence. Actual $\varepsilon$-achievability is exactly \begin{equation}\label{wsref-0-65-71-3a-73-69-6d-70-6c-65} \exists m\,[S(m)\wedge A(m,V^*-\varepsilon)]. \end{equation} Elimination decides this sentence and sample extraction constructs a witness when it is true. It does not replace sequential equilibrium by a truthful or designer-favorable equilibrium.

If publicly specified primitive data $\xi$ vary semialgebraically, construct $\operatorname{Value}(\xi,v)$ by (eq:Value). Eliminating $v,m$ from \[ \exists v,m\,[\operatorname{Value}(\xi,v)\wedge S(\xi,m) \wedge A(\xi,m,v-\varepsilon)] \] returns a quantifier-free polynomial-sign criterion on $(\xi,\varepsilon)$. This is an effective exact characterization of the data on which the specified simple format achieves the guarantee. It permits explicit restrictions on prices, symmetry, messages, rounds, and information acquisition.

If the simple class is nonempty, let $V_S$ be its supremum. The inequality $V_S\ge V^*-\varepsilon$ is weaker at equality: the supremum may be unattained. A strict gap $V^*-V_S<\varepsilon$ suffices. At equality, actual attainment of that threshold in $S$ is required. Formula (eq:simple) treats this boundary exactly. Sections sec:bounds--sec:simple, together with the equilibrium construction, prove Theorem Theorem (Exact robust design in the declared class).

Imported algebraic algorithms and bit complexity

We use complete real-closed-field quantifier elimination and algebraic sample-point extraction. Basu [Basu2014], Theorem 2.4 and Section 2.1.2 (PDF page 6), give the standard CAD arithmetic complexity. Theorem 2.27 (PDF page 16) gives effective elimination with quantifier-block and free-variable counts, including integer intermediate and output bit-size bounds. The detailed underlying algorithm is cited there as reference [25].

Let $k$ be the total number of real variables in the fully compiled formula, $s$ its polynomial-predicate count, $d_0$ the maximum degree, and $L$ the rational coefficient bit length. These counts include legality and support cases, primitive-graph variables, continuation and tremble variables, feasibility constraints, all optimization quantifiers, and free public-data coordinates. They are not merely the number of bidders or advertised price parameters. General CAD has an arithmetic bound of the form \[ (s d_0)^{\,2^{O(k)}}. \] For the bit statement, use dense polynomial encoding and clear constant rational denominators by positive integer multiples. A polynomial has at most $N=\binom{k+d_0}{k}$ coefficients; if their numerators and denominators have at most $L$ bits, the cleared integer coefficients have at most $L_{\mathbb Z}=(N+1)L$ bits. Put each compiled formula in prenex form, renaming bound variables apart and counting the renamed variables in $k$. Each atom becomes a sign condition on one of at most $s$ polynomials or a disjunction of two such conditions; $d_0$ is unchanged and the formula length grows by a constant factor. For a prenex formula with $\ell$ free variables and quantifier blocks of sizes $k_i$, with $\Pi_i$ the product over the blocks, Basu, Pollack, and Roy [BPR1996], Theorem 1.3.1 (pp. 1004--1005), compute an equivalent quantifier-free formula with $s^{(\ell+1)\Pi_i(k_i+1)}d_0^{(\ell+1)\Pi_iO(k_i)}$ arithmetic operations in the coefficient ring. The output is a disjunction of at most that many conjunctions, each of at most $s^{\Pi_i(k_i+1)}d_0^{\Pi_iO(k_i)}$ sign conditions on polynomials of degree at most $d_0^{\Pi_iO(k_i)}$. Since $\ell+\sum_ik_i\le k$, the exponent of $s$ is at most $2^k$. Their algorithms are well behaved $p.~1004$: over $\mathbb Z$, all intermediate and output integers have bit size at most the input bit size times the algebraic part $d_0^{(\ell+1)\Pi_iO(k_i)}$ of the complexity, and counting Boolean operations multiplies the operation count by a factor linear in the length of the input formula. At fixed total variable and degree bounds, the effective-QE theorem's operation counts are polynomial in predicate count and formula length, and its intermediate integer lengths are polynomial in coefficient length. Exact integer arithmetic therefore gives polynomial bit cost in the dense input size and the requested rational accuracy input length. A rational $\varepsilon=a_\varepsilon/b_\varepsilon$ enters through one more variable $t$ and the atom $b_\varepsilon t-b_\varepsilon v +a_\varepsilon=0$. A formula containing $V^*$ is used with $V^*$ replaced by a variable $v$ constrained by $\operatorname{Value}(v)$, as in Section sec:simple.

For the bit statement, algebraic witnesses are taken from the quantifier-free output rather than from the cylindrical construction of Lemma Lemma (Exact sample witnesses). Let $\Psi(y)$, $y\in\mathbb R^\ell$, be satisfiable and quantifier free, with $s'$ polynomials in $\mathbb Z[y]$ of degree at most $d'$ and coefficient bit size at most $L'$. The sample-points subroutine of [BPR1996], Section 3.1.3 (pp. 1028--1029), returns univariate representations $(f,g_0,\dots,g_\ell)\in\mathbb Z[T]^{\ell+2}$. Their associated points $(g_1(\theta)/g_0(\theta),\dots,g_\ell(\theta)/g_0(\theta))$, with $\theta$ a real root of $f$ and $g_0(\theta)\ne0$, meet every connected component of the realization of every realizable sign condition on these polynomials $p.~1007$. The univariate sign determination of Section 3.1.4.3 $p.~1030$ gives the Thom encoding of each such root, that is, the signs of the derivatives of $f$ there, and the signs of the $s'$ polynomials at the associated point. These two steps are the well-behaved algorithm of Theorem 1.3.3 described in Section 3.2 $p.~1031$. They use $s'^{\,\ell+1}d'^{\,O(\ell)}$ arithmetic operations, and the polynomials $f,g_j$ have degree $O(d')^\ell$ and integer coefficients of bit size $L'd'^{\,O(\ell)}$ (proof of Theorem 4.1.1, p. 1031). The set defined by $\Psi$ is a nonempty union of such components, so evaluating $\Psi$ on the computed sign vectors selects an associated point that satisfies $\Psi$. Its univariate representation and Thom encoding form the algebraic witness. For an elimination output as above, $s'$ is polynomial in $s$, while $d'$ and $L'/L_{\mathbb Z}$ are bounded at fixed $k$ and $d_0$. Hence the witnesses, including $V^*$ as the witness of the one-variable formula (eq:Value), have descriptions of polynomial size and are computed at polynomial bit cost. The algorithm of Theorem Theorem (Exact robust design in the declared class) makes a bounded number of such eliminations and extractions. The bisection alternative adds the number of calls in (eq:bisection). After $n$ halvings each queried threshold is the initial lower endpoint plus $j2^{-n}$ times the initial width, with $0\le j\le2^n$, so its bit length is linear in $n$ and in the bit lengths of the initial endpoints.

This proves tractability at fixed compiled structural size. It proves no polynomial bound in unrestricted game size, no efficiency claim as the structural dimension varies, and no strict fixed-parameter-tractability claim. All formulas are explicitly constructed from finite input before the imported algorithm is applied. A full CAD run for the all-friction family below has not been performed or claimed.

A nonlinear family with all frictions active

Two bidders compete for one object, with zero seller cost. Bidder $i$ initially knows $(z_i,\beta_i)$. Here $z_i\in\{0,1\}$, while $\beta_i$ independently selects an initial cash budget $1$ or $2$, each with probability $1/2$. Budgets are independent across bidders and independent of the $z$'s. The joint signal law is \[ \pi_\rho(0,0)=\pi_\rho(1,1)=\frac{1+\rho}{4},\qquad \pi_\rho(0,1)=\pi_\rho(1,0)=\frac{1-\rho}{4}, \qquad \rho\in[1/4,1/2]. \] All profiles have positive probability, and the signals are correlated. If $i$ wins, its monetary value is \[ v_i=\frac14+z_i+\frac32z_j. \] Thus the realized value depends on the other's true signal even after allocation; this is genuine interdependence. Entry costs $1/32$ cash, and a further optional private signal costs $1/32$ cash, both paid to outside parties. The acquired binary report of $z_j$ has accuracy $\tau\in[9/10,19/20]$, with noises independent conditional on the true signals. Both reports have positive probability in every state.

Bidder $i$'s monetary utility has $\eta_i\in[1/100,1/50]$ and is \begin{equation}\label{wsref-0-65-71-3a-75-74-69-6c-69-74-79-65-78-61-6d-70-6c-65} U_\eta(x)= \begin{cases} (1+4\eta)x+4\eta,&x<-2,\\ x-\eta x^2,&-2\le x\le3,\\ (1-6\eta)x+9\eta,&x>3. \end{cases} \end{equation} Values and first derivatives agree at the endpoints. The derivative decreases from $1+4\eta$ to $1-6\eta>0$ on the middle interval and is constant outside. Hence the extension is globally increasing and concave and is strictly concave on the relevant monetary outcomes. It is rational-semialgebraic and $U_\eta(0)=0$. Terminal utility is applied to value received minus net seller payments minus the actual external cash costs; these costs are not subtracted again in utility units.

Use an independent fair public priority draw, and offer the object serially at price $1$, once to each bidder. The calculations below condition on whichever bidder is drawn first. An invited bidder may decline entry at no cost, or enter, optionally buy the report, and accept or reject. It never receives another offer. Acceptance requires the actual affordable cash payment. Seller revenue excludes the external fees.

Strict acquisition by a low-signal, high-budget first bidder

For the first bidder with $z_i=0$ and budget $2$, put \[ p=\Pr(z_j=1\mid z_i=0)=\frac{1-\rho}{2}\in[1/4,3/8]. \] At $\tau=9/10$, consider the complete continuation: enter, acquire, and accept exactly after a positive report. Its terminal monetary outcomes $Z$ are \[ \frac{11}{16}\quad(z_j=1,+),\qquad -\frac{13}{16}\quad(z_j=0,+),\qquad -\frac1{16}\quad(-). \] The probabilities are respectively $9p/10$, $(1-p)/10$, and $9/10-4p/5$. Direct substitution gives \begin{equation}\label{wsref-0-65-71-3a-61-63-71-75-69-73-69-74-69-6f-6e-6d-6f-6d-65-6e-74-73} \mathbb E Z=\frac34p-\frac{11}{80},\qquad \mathbb E Z^2=\frac{456p+89}{1280}. \end{equation} In particular $\mathbb E Z\ge1/20$, while \[ \eta\,\mathbb E Z^2 \le\frac1{50}\frac{260}{1280}<\frac1{200}. \] Therefore $\mathbb E U_\eta(Z)>0$ throughout the parameter range. For example, at $\rho=1/3$, the two moments are $9/80$ and $241/1280$.

The positive-report posterior is \[ r_+=\frac{\tau p}{\tau p+(1-\tau)(1-p)}\ge\frac34, \] and the negative-report posterior satisfies \[ r_-=\frac{(1-\tau)p}{(1-\tau)p+\tau(1-p)}\le\frac1{16}. \] The bounds follow by monotonicity of the likelihood odds in $p,\tau$; their extreme values occur at $(p,\tau)=(1/4,9/10)$ and $(3/8,9/10)$, respectively. After both fees are sunk, acceptance gives $11/16$ or $-13/16$; rejection gives $-1/16$. At posterior $r$, the utility difference is exactly \[ \frac34(2r-1)-\eta\,\frac{168-48r}{256}. \] For a positive report, $r\ge3/4$ gives $168-48r\le132$. Its monetary part is at least $3/8$, and the absolute risk correction is at most $\eta(132/256)<1/50$, so acceptance is strict. For a negative report, the monetary part is already negative and the risk correction makes acceptance worse; rejection is strict.

Increasing $\tau$ above $9/10$ improves this policy's utility. Its derivative with respect to $\tau$ is \[ p[U_\eta(11/16)-U_\eta(-1/16)] +(1-p)[U_\eta(-1/16)-U_\eta(-13/16)]>0. \] This moves probability from a false acceptance to rejection, and from rejection to a correct acceptance. Thus the positive entry-and-acquisition payoff is uniform over the entire stated accuracy range.

Without acquiring information, entry followed by acceptance has mean monetary outcome \[ \frac32p-\frac{25}{32}\le-\frac7{32}. \] On all these outcomes $U_\eta(x)\le x$, so its expected utility is negative. Entering and rejecting yields $U_\eta(-1/32)<0$; mixing these choices cannot improve their expected-utility maximum. Declining entry yields zero. The strictly positive acquiring policy, whose report-contingent choices are strict, therefore forces this type to enter and acquire in every sequential equilibrium. Full continuation rationality at the first invitation compares these complete policies using the true conditional prior; no favorable off-path belief is assumed. Once these actions are taken, both reports occur with positive probability and their Bayesian continuation choices are the strict ones above. Later bidder behavior cannot change this bidder's payoff because it never receives another offer.

Its largest cash requirement is \[ 1+\frac1{32}+\frac1{32}=\frac{17}{16}\le2. \] A budget-$1$ bidder cannot fund price $1$ even without acquiring, since entry plus acceptance costs $1+1/32>1$. Acquisition does not create cash. Entry would then only incur a loss, so this bidder strictly declines entry. Liquidity therefore changes actual conduct.

A worst-equilibrium same-class guarantee

A first bidder with $z_i=1$ and budget $2$ has value at least $5/4$. It strictly enters and accepts without information: entry and acceptance give strictly positive monetary surplus in every state, and acceptance is optimal after any report. Information cannot improve that already optimal decision and its strictly positive cash cost reduces utility. This type has probability $1/4$. Thus every sequential equilibrium in every displayed environment gives seller revenue at least $1/4$; later sale payments are nonnegative. This uses the same feasible class on both sides. The information acquisition is strictly active on a positive-probability type, changes its action with the report, and remains costly. Correlation, interdependence, strict monetary risk aversion, and conduct-changing private liquidity all coexist.

A continuous design family containing this mechanism lets the two serial prices vary independently over $[3/4,5/4]$, and chooses the public priority order with probability $\lambda_0\in[1/4,3/4]$. These are three real mechanism parameters. Each bidder has finitely many entry, acquisition, and accept/reject choices. Initial private signals, budgets, and acquired reports remain private, while the bidder remembers its own choices and observed priority and refusals. Accepting is permitted only when the actual cash payment can be made. Cash-action legality changes at finitely many affine comparisons between the offered price and remaining cash; the guards agree within each information set. The game family is consequently a finite union of rational semialgebraic legal strata with perfect recall. The environment parameters $(\rho,\tau,\eta_1,\eta_2)$ vary over the stated rational intervals. Nature laws, payoffs, and seller-independent cash costs all have rational-semialgebraic descriptions. The seller uses the announced prices and observed acceptances, not hidden state labels or unknown environment parameters.

The declared participation constraint is interim, with benchmark $u_i^{\mathrm{out}}\equiv0$ in (eq:interimIR). Interim participation holds in every equilibrium of this family. At a bidder's first invitation, no entry guarantees zero for every hidden state and every later play. Sequential rationality gives nonnegative expected actual utility at that information set. Averaging over invitations and the public priority draw preserves the inequality conditional on each initial private type. No invitation incurs no cost. Realized losses on some acquired-report branches are possible; the condition is interim participation, not outcome-by-outcome ex-post IR.

Scope and prior attempts

The canonical formulation asks for a stated collection of environments and a stated feasible mechanism class. The result here covers the entire declared semialgebraic design continuum for arbitrary finite input templates, including all legal and Nature-support boundary strata. It is not a universal characterization across every unbounded auction tree or arbitrary unrepresented monetary utility. The environment specification is common knowledge within each bidders' game; the seller's rules remain independent of hidden environment and signal information except through actual observations.

The exact consistency condition keeps the mechanism and environment fixed, uses one common completely mixed assessment witness, and imposes no equilibrium requirement on that witness. Full continuation comparisons, true liquidity, endogenous entry and acquisition, and universal equilibrium participation and revenue are retained. The finite robust bound comes from actual cash constraints, not equilibrium continuity. The value and witness formulas distinguish a supremum from an attained maximum and actual simple-format achievability from an unattained supremal threshold. The explicit nonlinear family shows that the five frictions can be simultaneously substantive, with a same-class approximation guarantee.

The prior Ultra attempt [PriorUltra] proves a restricted harmonic posted-price guarantee with private values, free participation and information, private budgets and monetary risk under stronger outcome-by-outcome participation. Its stated limitations include interdependence, costly entry and acquisition, and the broader interim benchmark. The prior Pro attempt [PriorPro] supplies the attributed nonattainment example, equilibrium-selection obstructions, a fixed-entry selected-truthful-equilibrium lottery program, and a finite-catalogue bound conditional on supplied worst-equilibrium enclosures.

The present proof explicitly constructs the full equilibrium and feasibility formulas and applies an imported complete real-algebraic algorithm to the entire stated design class. Exact symbolic sequential-equilibrium computation and real quantifier elimination have established precedents [KW1982,GEN2024,Basu2014]. The mathematical algorithm theorem is proved, but a full CAD execution for the all-friction family and practical large-game performance are not claimed.

\section*{Use of AI tools}

The author used research AI agents that the author built and configured (GPT-6 Astra max, Claude Opus 5.5 max and GPT-6 Astra Pro) during the proof work, for proof search and construction, proof checking, translation, Python computation and similar tasks. The final manuscript was written, and the proofs were checked, by the human author. All responsibility for this work rests with the author personally.

References

• [KW1982] David M. Kreps and Robert Wilson. Sequential Equilibria. Econometrica 50$4$ $1982$, 863--894. doi:10.2307/1912767. Stanford author publication record. The positive common initial Nature-probability convention appears on page 868.
• [Bonanno2015] Giacomo Bonanno. Game Theory: An Open Access Textbook with 165 Solved Exercises. University of California, Davis, 2015. arXiv:1512.06808v1, 21 December 2015.
• [GEN2024] Moritz Graf, Thorsten Engesser, and Bernhard Nebel. Symbolic Computation of Sequential Equilibria. Proceedings of AAMAS 2024. arXiv:2402.04452v1, 6 February 2024; published conference PDF.
• [Basu2014] Saugata Basu. Algorithms in Real Algebraic Geometry: A Survey. arXiv:1409.1534v1 $2014$. Imported algorithmic bounds: Theorem 2.4 and Section 2.1.2 (PDF page 6), and Theorem 2.27 (PDF page 16). The latter gives quantifier-block and integer bit-size bounds.
• [BPR1996] Saugata Basu, Richard Pollack, and Marie-Françoise Roy. On the Combinatorial and Algebraic Complexity of Quantifier Elimination. J. ACM 43$6$ $1996$, 1002--1045. doi:10.1145/235809.235813.
• [PriorUltra] Prior catalogue attempt, attributed to GPT 6 Astra Ultra. Finite posted-price guarantees with correlation, risk, and liquidity. First posted 9 October 2026; marked unresolved. Prior Ultra source.
• [PriorPro] Prior catalogue attempt, attributed to GPT 6 Astra Pro. D44-34: Robust auction design with interacting frictions. First posted 9 October 2026; marked unresolved. Prior Pro source. Source of Example Example (Prior tie-driven nonattainment).