← back to the atlas

d4-conf-ecai-2025-0549 (d4-conf-ecai-2025-0549)

Answer: —

The anchor (named result in the paper)

Theorem 4 — class: algorithmic

PDF text-layer excerpt — equations and symbol order may be approximateGiven any instance I = N, E, (≻i)i∈N where (N, E) is an acyclic acceptability graph, I is ⃗k convergent in a poly- nomial number of moves even if, for any i ∈N, ki = 1. Moreover, any agent can be involved in at most |N|2/4 moves along the dynam- ics.

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

The continuous mirror question, as graded

For an atomless probability space \((X,\nu)\) with a bounded-degree, port-labelled treeing, a finite type set \(T\), and rational type masses \(\mu_t=\nu(\{x:\theta(x)=t\})\), can one construct a measurable matching \(M\) along treeing edges such that the set of 1-blocking edges has measure zero? The computational version asks for an algorithm under a fixed effective finite-presentation model for the treeing and matching.

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

Use the following rational interval presentation. Let \(X=[0,1)\) with Lebesgue probability measure \(\nu\). An input lists \(r\) records \((I,c,p,q)\), with rational half-open interval \(I\), rational translation \(c\), and ports \(p,q\in\{1,\ldots,m\}\): for \(x\in I\), its port-\(p\) neighbor is \(x+c\), whose return port is \(q\). Inverse records are included; the records are promised to define a simple, acyclic graph with distinct ports at each vertex and degree at most \(m\).
A rational interval partition specifies \(\theta:X\to T\). Each type specifies its available ports and a strict ranking of them, consistent with the graph; every neighbor is preferred to being unmatched.
A society is given by its support: the list of the \(\tau\) types with positive mass, each mass \(\mu_t=\nu(\theta^{-1}(t))\) a binary rational, with \(\sum_t\mu_t=1\). Here \(\tau\) is the support size, not the number of possible types. Let \(L\) be the total input bit length.
Represent a matching by a finite circuit taking \(x\) as input, using rational affine operations, floor, comparisons, and conditional selection, and returning an available port or \(0\). Port \(0\) means unmatched; otherwise the selected neighbor is \(M(x)\). Require \(M(M(x))=x\) almost everywhere, with \(M(x)=x\) when unmatched.
For an unselected edge \(\{x,y\}\), call it \(1\)-blocking if both endpoints strictly prefer each other to their current partners, including the unmatched option. Its blocking-edge set \(B_M\) must satisfy \(\eta(B_M)=0\), where \(\eta(F)=\tfrac12\int_X\deg_F(x)\,d\nu(x)\).

Can such a matching circuit be constructed in time polynomial in \(m,\tau,r,L\), or is this construction problem \(\mathrm{NP}\)-hard under polynomial-time Turing reductions?

For finite forests with strict preferences, every sequence of blocking-pair moves terminates after at most \(n^3/8\) moves, yielding polynomial-time stable-matching construction ([finite convergence result](https://journals.sagepub.com/doi/full/10.3233/FAIA251234)).
For acyclic locally countable Borel graphs of minimum degree three generating a measure-hyperfinite equivalence relation, measurable perfect matchings exist ([measurable matching result](https://www.math.cmu.edu/users/math/clintonc/onlinepapers/matching.pdf)); this imposes no preference stability or finite-presentation complexity guarantee. No result settling the stated circuit-construction problem was located.

Modeling choices made when packaging the task

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

Partial resolution: all degree-two inputs are polynomial-time solvable

The unrestricted construction problem remains unresolved. I prove two additional results:

The first result extends the single-translation path case in the notes. The second gives a space bound, but does not establish the polynomial-time construction requested in the general case.

1. Exact finite reduction and the canonical matching

Let $s$ be the number of intervals in the partition specifying $\theta$. Fix $D$ to be the least common multiple of the denominators of all record endpoints, translations, and type-partition endpoints. Include the endpoints $0,1$ when necessary.

Because the logarithm of a least common multiple is bounded by the sum of the logarithms of its arguments,

$$ \log_2 D\leq L. $$

For $u\in[0,1)$ and $i\in\{0,\ldots,D-1\}$, put

$$ \phi_u(i)=\frac{i+u}{D}. $$

Every $x\in X$ has a unique representation of this form, with

$$ i=\lfloor Dx\rfloor, \qquad u=Dx-\lfloor Dx\rfloor. $$

After clearing denominators, a record has interval $[A/D,B/D)$ and translation $C/D$, where $A,B,C$ are integers. For every $u\in[0,1)$,

$$ \phi_u(i)\in[A/D,B/D) \quad\Longleftrightarrow\quad A\leq i<B, $$

and

$$ \phi_u(i)+C/D=\phi_u(i+C). $$

Consequently, every fiber has exactly the same port-labelled graph and preferences. Let $H$ denote this graph on

$$ V=\{0,\ldots,D-1\}. $$

Its records are integer interval translations $i\mapsto i+C$, applicable for $A\leq i<B$. Inverse records describe the same undirected edges.

The promises imply that $H$ is a simple finite forest, with distinct ports and the stated degree bound. A violation in $H$ would occur in every fiber. The type partition likewise gives preferences on $H$ independent of $u$. Half-open intervals make these statements valid also when $u=0$.

In particular, all connected components of the original graph are finite.

Lemma 1: uniqueness on finite forests

Every finite forest with strict preferences, with every neighbor preferred to being unmatched, has exactly one stable matching.

Proof. Induct on the number of vertices. The edgeless case is immediate.

At every nonisolated vertex, direct an arrow to its first-choice neighbor. Following arrows eventually reaches a directed cycle. Simplicity excludes a loop, and the forest condition excludes a directed cycle of length at least $3$. Thus some adjacent vertices $a,b$ are each other’s first choice.

Every stable matching must select $\{a,b\}$: otherwise both endpoints strictly prefer this edge to their assignments.

Delete $a,b$ and restrict the remaining preference lists. By induction, the residual forest has a unique stable matching $S'$. Adding $\{a,b\}$ gives a stable matching: edges inside the residual forest cannot block, and any edge incident to $a$ or $b$ is rejected by that endpoint, which receives its first choice.

Conversely, the restriction of any original stable matching to the residual forest must be stable there. This proves existence and uniqueness. $\square$

Write $p_i$ for the selected port at vertex $i$ in this unique matching, with $p_i=0$ when unmatched. The circuit

$$ x\longmapsto p_{\lfloor Dx\rfloor} $$

is a valid matching circuit: implement its finite table using comparisons and conditional selections. It is a matching on every fiber and has no blocking edges anywhere.

Expanding $H$ and applying the preceding induction constructively takes time polynomial in $D,m,\tau,r,L$, hence exponential time in $L$.

Almost-everywhere uniqueness

The canonical circuit is also the unique solution up to a null set.

Indeed, let $E$ be the null set where an admissible circuit fails the involution requirement. Let $V_B$ be the set of vertices incident to a blocking edge. Since blocking degree is a nonnegative integer,

$$ \eta(B_M)=0 \quad\Longrightarrow\quad \nu(V_B)=0. $$

For any measurable $N\subseteq X$,

$$ \nu(N)=\frac1D\sum_{i=0}^{D-1} \int_0^1\mathbf 1_N(\phi_u(i))\,du. $$

Applying this identity to $E\cup V_B$ shows that, for almost every $u$, every vertex of its finite fiber avoids both exceptional sets. On such a fiber the circuit is a stable matching of $H$, so Lemma 1 forces it to equal the canonical matching.

The society masses impose no additional constraint on the matching in the stated task.

2. From vertex queries to matching circuits

A stable-port query asks for $p_i$, given the presentation and a binary index $i\in V$. The index has $O(L)$ bits.

The following implication will turn the degree-two algorithm below into a circuit constructor.

Lemma 2: compiling a polynomial-time query algorithm

If stable-port queries for a class of presentations have a deterministic polynomial-time algorithm, then stable matching circuits for that class can be constructed in polynomial time.

Proof. Fix the presentation and leave only the binary index variable. Unroll the polynomial-time query algorithm into a Boolean circuit, hardwiring the presentation. A polynomial number of computation steps, each represented by a polynomial-size configuration and transition circuit, gives a polynomial-size circuit constructible in polynomial time.

The permitted operations recover the index and its bits. Put

$$ k=\lfloor Dx\rfloor. $$

For $0\leq j<\lceil\log_2D\rceil$, its $j$-th bit is

$$ b_j= \left\lfloor\frac{k}{2^j}\right\rfloor - 2\left\lfloor\frac{k}{2^{j+1}}\right\rfloor. $$

Boolean negation is $1-b$, and conjunction can be implemented by testing whether the sum of two Boolean inputs equals $2$. Conditional selection converts comparison outcomes to Boolean values when needed. Finally, decode the output bits into the integer port.

The resulting circuit returns $p_{\lfloor Dx\rfloor}$ on all of $X$, so Section 1 verifies the matching and stability requirements everywhere. The case $D=1$ is immediate. $\square$

3. Polynomial-time connectivity tools for interval translations

The degree-two algorithm uses the following published theorem.

Agol–Hass–Thurston orbit-counting theorem. Given $k$ order-preserving or order-reversing bijections between integer subintervals of $\{1,\ldots,N\}$, the number of equivalence classes generated by these pairings and their inverses can be computed in time polynomial in $k$ and $\log N$. This is [Theorem 12 of *The Computational Complexity of Knot Genus and Spanning Area*](https://arxiv.org/pdf/math/0205057).

Here all pairings are translations. Their equivalence classes are precisely the connected components of the graph represented by the pairings. Indexing from $0$ instead of $1$, and using half-open integer intervals instead of inclusive intervals, changes only the notation.

We need two consequences, whose reductions are proved next.

Lemma 3: testing whether a component meets an interval union

Suppose a graph $G$ on $\{0,\ldots,N-1\}$ is specified by integer interval translations. Given a vertex $v$ and a set $S$ represented as a union of $b$ integer intervals, one can decide whether the component of $v$ meets $S$ in time polynomial in the pairing count, $b$, and $\log N$.

Proof. Merge overlapping intervals of $S$, and add a new vertex $z=N$.

For each nonempty interval $[a,b)$ in $S$, add:

These additions join every vertex of $S$ to $z$. Let $K$ be the augmented graph, and let $K'$ additionally contain $\{v,z\}$.

If the original component of $v$ meets $S$, then $v,z$ are already connected in $K$. Otherwise none of the added edges touches that component, so $v,z$ are disconnected in $K$. Therefore,

$$ \operatorname{comp}(K')=\operatorname{comp}(K) $$

holds exactly when the original component meets $S$; in the other case the component count decreases by $1$.

Both counts are provided by the orbit-counting theorem. The construction adds $O(b)$ pairings and uses integers with $O(\log(N+1))$ bits. $\square$

Taking $S$ to be a singleton gives polynomial-time connectivity tests.

Lemma 4: distance parity in a succinct forest

For an interval-translation forest $G$, the parity of the distance between two connected specified vertices can be computed in polynomial time.

Proof. Form the bipartite double cover on vertices $(i,\epsilon)$, where $\epsilon\in\{0,1\}$. Every original edge $\{i,j\}$ gives edges

$$ \{(i,0),(j,1)\}, \qquad \{(i,1),(j,0)\}. $$

Encode $(i,\epsilon)$ by $i+\epsilon N$. An original pairing $i\mapsto i+C$ on $[A,B)$ gives the two translation pairings

$$ i\mapsto i+C+N \quad\text{on }[A,B), $$

and

$$ i+N\mapsto i+C \quad\text{on }[A+N,B+N). $$

Thus the cover has a polynomial-size interval presentation.

The unique simple path between the specified vertices switches sheets at each edge. Moreover, every closed walk in a forest has even length: removing any edge splits the forest into two parts, so a closed walk crosses that edge an even number of times. Hence a walk between the specified vertices has the same parity as their simple path.

It follows that $(v,0)$ is connected to $(a,0)$ exactly when the distance from $v$ to $a$ is even. Apply Lemma 3 to the singleton $(a,0)$. $\square$

The auxiliary graphs in Lemmas 3 and 4 need not satisfy the original port promises. The orbit-counting theorem has no such requirement.

4. Polynomial-time construction for every degree-two input

Assume now that $H$ has maximum degree at most $2$. Its nontrivial components are paths, but their numerical ordering may be unrelated to their path ordering.

For each nonisolated vertex $v$, let $f(v)$ be its first-choice neighbor. Define an undirected subforest $F$ by retaining exactly the edges selected as a first choice by at least one endpoint:

$$ E(F)= \bigl\{\{v,w\}\in E(H): f(v)=w\text{ or }f(w)=v\bigr\}. $$

Let

$$ E_0=E(H)\setminus E(F). $$

4.1 Every nontrivial component of $F$ has one mutual first-choice edge

A nonisolated vertex retains its chosen edge, so a nontrivial component of $F$ with $n$ vertices contains exactly $n$ first-choice arrows. Being a tree, it has $n-1$ undirected edges.

Each edge carries either one or two arrows. If $d$ edges carry two arrows, counting arrows gives

$$ n=(n-1)+d, $$

so $d=1$.

Thus there is exactly one mutual first-choice edge in each nontrivial component of $F$. Denote it by $\{a,b\}$.

Removing this edge leaves two paths, each rooted at its corresponding endpoint. At every other vertex the first-choice arrow points toward that endpoint. To justify the latter statement, following arrows must reach a mutual first-choice edge; the unique such edge is $\{a,b\}$. In a tree, the route toward it is unique.

4.2 The internal matching of $F$

Select $\{a,b\}$ in every nontrivial component. On each arm, number vertices by their distance $d$ from its sink endpoint, and select edges between distances

$$ 1,2;\quad 3,4;\quad 5,6;\quad\ldots $$

Call this matching $J$, writing $J(v)=\bot$ when $v$ is unmatched.

Equivalently:

This is stable within $F$. An unselected arm edge joins distances $d,d+1$ with $d$ even. Its even-distance endpoint receives its first choice and rejects the unselected edge. The sink edge is selected.

Notice also that every matched endpoint of a component of $F$ receives its first choice.

4.3 The discarded edges form a matching

If $\{v,w\}\in E_0$, neither endpoint chooses the other first. Each endpoint therefore has another neighbor. Since its degree is at most $2$, each endpoint is incident to exactly one edge of $E_0$.

Consequently, $E_0$ is a matching. Its endpoints have degree $1$ in $F$.

Extend $J$ by selecting precisely the edges of $E_0$ whose two endpoints are unmatched under $J$. Call the resulting matching $S$.

This extension is feasible because $E_0$ is a matching. It is stable:

Lemma 1 therefore identifies $S$ as the unique stable matching of $H$.

4.4 Succinctly presenting $F$ and its sink endpoints

The preceding description has not yet supplied a polynomial-time algorithm: the paths can be exponentially long. We now implement it without traversing them.

For each original integer record $i\mapsto i+C$ on $[A,B)$, split its domain at:

On each resulting interval, both endpoint types are constant. Hence one can decide whether the source port is its endpoint’s first choice and whether the return port is the other endpoint’s first choice.

Retain that subrecord for $F$ exactly when at least one test holds. Record its domain as part of a set $Z$ exactly when both tests hold.

Because inverse records are present, $Z$ is precisely the set of endpoints of mutual first-choice edges. This produces $O(rs)$ interval pieces before merging. All arithmetic and sorting take polynomial time.

Thus both $F$ and the interval union $Z$ have polynomial-size presentations.

4.5 Computing $J(v)$ in polynomial time

An isolated vertex of $H$ has $J(v)=\bot$. Otherwise use the following procedure.

Locate the sink edge. The component of $v$ in $F$ meets $Z$ in exactly two vertices. By Lemma 3, the predicate

$$ \text{the component of }v\text{ meets }Z\cap[0,k+1) $$

is polynomial-time computable and monotone in $k$. Binary search finds its smallest true index $a$ in $O(\log D)$ tests. Then $b=f(a)$ is the other sink endpoint.

Determine the relevant arm. Delete the singleton edge $\{a,b\}$ from the interval presentation of $F$. To remove every record describing this edge, split applicable domains around the corresponding source index and discard that singleton. This increases the presentation size only polynomially.

In the resulting forest, $v$ is connected to exactly one of $a,b$. Determine that endpoint, say $a_v$, using Lemma 3.

Determine the distance parity. Apply Lemma 4 to compute the parity of the distance from $v$ to $a_v$.

If the distance is even, return

$$ J(v)=f(v). $$

If it is odd, inspect the available neighbors other than $f(v)$. There is at most one. It is the next vertex farther from the sink exactly when it chooses $v$ as its first choice. Return that neighbor if it exists; otherwise return $\bot$.

These rules implement exactly the internal matching in Section 4.2. All local neighbor and preference queries use the supplied records and partition, so they take polynomial time.

4.6 Computing the final stable port

First compute $J(v)$.

If it is a neighbor, return its corresponding port. Otherwise inspect whether $v$ has an incident edge $\{v,w\}\in E_0$. There is at most one. Select it exactly when $J(w)=\bot$; if no such selection is possible, return port $0$.

The algorithm makes $O(\log D)$ orbit-based tests for each internal-partner computation. Every tested presentation has polynomially many pieces and an integer universe of size at most $2D+1$. Since $\log D\leq L$, its total running time is polynomial in $m,\tau,r,L$.

Applying Lemma 2 proves the promised result:

Theorem. Stable matching circuits can be constructed in polynomial time for every promised presentation whose graph has maximum degree at most $2$, without any restriction on the number or values of its translations.

As a separate computational check of the combinatorial rule, I compared it with direct enumeration of stable matchings for all $1{,}023$ endpoint-consistent preference sequences on paths of sizes $2$ through $11$. Every result agreed. The proof above establishes correctness independently of that check.

5. Polynomial-space stable-port queries in the general case

The next result allows arbitrary branching. Its running time can be exponential.

For adjacent vertices $v,u$ of a finite preference-labelled tree, let $T(v\mid u)$ be the component containing $v$ after deleting $\{v,u\}$. Define

$$ A(v\mid u)=1 $$

exactly when $v$ strictly prefers $u$ to its partner in the unique stable matching of $T(v\mid u)$. An unmatched vertex prefers every original neighbor to being unmatched.

5.1 A directed-offer recurrence

The messages satisfy

$$ A(v\mid u) = \neg \bigvee_{\substack{w\in N_H(v)\setminus\{u\}\\w\succ_v u}} A(w\mid v), $$

where $w\succ_v u$ means that $v$ prefers $w$ to $u$, and an empty disjunction is false.

Moreover, in a tree rooted at $v$, the stable partner of $v$ is its most preferred neighbor $w$ satisfying $A(w\mid v)=1$, or unmatched if there is no such neighbor.

Here is a proof, including the interaction between a chosen child and its descendants.

Proof. Induct on the size of a rooted tree. For each child $w$ of the root $v$, let $S_w$ be the unique stable matching of the child subtree, and say that $w$ offers to $v$ when it prefers $v$ to its partner in $S_w$.

If no child offers, leave $v$ unmatched and use all the matchings $S_w$. Every edge incident to $v$ is rejected by its child endpoint, and all other edges are stable within their child subtrees.

Otherwise let $w_*$ be the most preferred offering child. Match $v,w_*$. Use $S_w$ on every other child subtree. In the chosen child subtree, delete $w_*$ and use the stable matching of each subtree rooted at a child $z$ of $w_*$.

By the induction hypothesis, the partner of $w_*$ in its standalone matching $S_{w_*}$ is its best offering child, if one exists. Since $w_*$ offers to $v$, it prefers $v$ to every offering child $z$. Thus an edge $\{w_*,z\}$ cannot block: either $z$ does not offer, or $w_*$ prefers its new partner $v$.

For an edge $\{v,w\}$ with $w\neq w_*$, either $w$ does not offer or $v$ prefers $w_*$ to $w$. It cannot block either. All remaining edges lie within the stable subtrees used in the construction.

The constructed matching is therefore stable. Lemma 1 proves that it is the unique stable matching, establishing the root-partner assertion.

Apply that assertion to $T(v\mid u)$. Its root partner is the best offering neighbor other than $u$. The vertex $v$ prefers $u$ to this partner exactly when no neighbor ranked above $u$ offers. This is the displayed recurrence. $\square$

5.2 Counting a rooted component with small working space

The size

$$ s(v\mid u)=|T(v\mid u)| $$

can be computed using polynomial working space, without retaining its vertices.

Delete the edge $\{v,u\}$ and order each remaining vertex’s incident edges cyclically by port number. For an oriented edge $(a,b)$, define its successor to be $(b,c)$, where the port to $c$ is the cyclic successor of the port from $b$ back to $a$.

For a nontrivial finite tree, this permutation has one cycle containing every oriented edge. To prove this, start with a single edge, whose two orientations form one cycle. Adding a leaf inserts its two edge orientations consecutively into the cycle at its attachment vertex. Every finite tree can be built by successive leaf additions, proving the assertion.

Starting with any oriented edge in $T(v\mid u)$, iterate until it returns. If the cycle length is $\ell$, then

$$ s(v\mid u)=1+\ell/2. $$

If the component is isolated, its size is $1$.

The simulation stores only the current and initial oriented edges, a counter bounded by $2D$, and temporary data for record queries. All require polynomially many bits. Its time may be proportional to $D$.

5.3 Evaluating offers with a logarithmic-depth stack

A direct recursive evaluation of $A(v\mid u)$ could have depth proportional to $D$. Instead, separate one potentially large child from the others.

At a current message $(v,u)$, put $s=s(v\mid u)$. Its relevant children are the neighbors $w$ ranked above $u$. Their original rooted components $T(w\mid v)$ are disjoint subsets of $T(v\mid u)\setminus\{v\}$.

Hence at most one relevant child has size greater than $s/2$. Call it the heavy child, if it exists. Every other relevant child has size at most $s/2$.

Evaluate the other relevant children recursively, one at a time.

$$ A(v\mid u)=1-A(h\mid v). $$
Continue iteratively at $(h,v)$, recording the complementation in one bit instead of pushing another frame.

This last step may repeat along a long chain. It needs only the current message and a bit recording the parity of accumulated complementations. When that iterative computation reaches a value, complement it according to the recorded bit.

Every actual recursive call enters a component of size at most half the current size, and thus at most half the size at the beginning of its parent frame. Therefore the stack depth is at most

$$ 1+\lceil\log_2 D\rceil. $$

Each frame stores a constant number of vertex indices, sizes, counters, and bits. Component sizes are computed by Section 5.2. All neighbor and ranking operations use polynomial working space.

Finally, for a queried vertex $v$, evaluate $A(w\mid v)$ for each neighbor $w$ and return the port of the best offering neighbor, or $0$ if none offers.

This proves:

Proposition. For arbitrary promised presentations, stable-port queries are computable using space polynomial in $m,\tau,r,L$.

This does not give a polynomial-time algorithm: the size computations and the message evaluation may inspect exponentially many vertices.

6. Why the degree-two argument stops at branching

The degree-two extension rule does not remain valid when a discarded edge can touch an interior vertex of an $F$-component.

Consider the tree with edges

$$ \{a,b\},\ \{a,v\},\ \{v,w\},\ \{v,u\},\ \{u,c\},\ \{c,d\}. $$

Give its vertices the strict preferences

$$ a:\ b\succ v, \qquad b:\ a, \qquad v:\ a\succ u\succ w, \qquad w:\ v, $$

and

$$ u:\ c\succ v, \qquad c:\ d\succ u, \qquad d:\ c. $$

Every neighbor is preferred to being unmatched. The maximum degree is $3$.

Its only edge selected as a first choice by neither endpoint is $\{v,u\}$. Thus the first-choice subforest $F$ has stable matching

$$ \{\{a,b\},\{v,w\},\{c,d\}\}, $$

with $u$ unmatched.

But $\{v,u\}$ blocks this matching: $v$ prefers $u$ to $w$, and $u$ prefers $v$ to being unmatched. Adding only discarded edges with two unmatched endpoints therefore fails.

The full tree instead has the stable matching

$$ \{\{a,b\},\{v,u\},\{c,d\}\}, $$

with $w$ unmatched. The unselected edges incident to $a,c$ are rejected by those vertices, and $\{v,w\}$ is rejected by $v$.

This is also an admissible rational interval example: assign the seven vertices consecutive grid cells of length $1/7$, give each oriented edge its corresponding singleton-cell translation record, and assign the displayed preferences by cells.

Thus the endpoint property used in Section 4 is essential. The offer recurrence handles this interaction correctly, but the polynomial-space evaluation does not supply the missing polynomial-time method.

7. Remaining question

The unrestricted target is still open in this write-up. What has been established is a polynomial-time constructor for the entire maximum-degree-two class, together with a polynomial-space query algorithm for arbitrary branching.

Neither result proves a polynomial-time constructor for all promised presentations, nor an $\mathrm{NP}$-hardness reduction under polynomial-time Turing reductions.

⟨structured verdict parsed — rendered above⟩

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

Verification report

The output establishes genuine partial results: a polynomial-time circuit constructor when the graph has maximum degree at most $2$, and a polynomial-space stable-port query algorithm for arbitrary promised inputs. I found no substantive mathematical error in either argument.

It does not resolve USER_TASK: neither a polynomial-time constructor for arbitrary branching nor an $\mathrm{NP}$-hardness reduction is supplied. The prover accurately acknowledges this limitation.

1. Finite reduction and uniqueness

The denominator reduction is correct. All listed rational endpoints and translations become integral multiples of $1/D$. The bound
$$ \log_2 D\leq L $$
follows from bounding the least common multiple by the product of the denominators encoded in the input. Computing $D$ and clearing denominators require only polynomially many bit operations.

For $0\leq u<1$, the displayed interval-membership equivalence is correct, including $u=0$. Translation by $C/D$ preserves $u$ and changes the index by $C$. The graph and preferences therefore agree across every fiber.

The graph promises transfer to $H$: a loop, duplicated neighbor with inconsistent ports, excessive degree, or cycle in $H$ would occur in its corresponding fibers. Every original connected component is consequently contained in a finite fiber. The proof does not incorrectly assert that a whole fiber must be connected.

Lemma 1 is correct. Following first-choice arrows in a finite nontrivial component produces a directed cycle. A loop is excluded by simplicity, and a cycle of length at least $3$ contradicts the forest condition. A mutual first-choice pair is therefore present and forced in every stable matching.

Deleting that pair and restricting preferences supports both directions of the induction:

This proves existence and uniqueness, including isolated vertices.

The table circuit and exponential-time bound are justified. A finite table can be implemented with the permitted comparisons and conditional selections. Expansion costs polynomial time in $D$ and the other parameters; the bound on $\log_2 D$ makes this at most exponential in input length.

Almost-everywhere uniqueness is also justified. The finite sum in the integration identity permits simultaneous exclusion of exceptional points at all $D$ indices for almost every $u$. On each remaining fiber, the circuit gives a genuine stable matching, and Lemma 1 applies. The argument correctly uses
$$ \eta(B_M)=0 $$
to conclude that the set of vertices incident to blocking edges is null.

The society masses impose no additional matching constraint in the task as stated.

2. Compilation of queries into circuits

Lemma 2 is correct. A deterministic polynomial-time algorithm on binary indices can be unrolled into a polynomial-size Boolean circuit, with the presentation hardwired.

The bit-extraction formula is correct for integral $k$. Boolean operations and output decoding can be implemented using the permitted affine operations, comparisons, and conditional selections. The constants involved have polynomial bit length.

The index lies in the required range for every $x\in[0,1)$, and the case $D=1$ is explicitly addressed. Thus the compilation produces the requested circuit representation, rather than merely an abstract algorithm.

3. Orbit-counting tools

The cited theorem is stated accurately and applies here. Theorem 12 of [Agol–Hass–Thurston](https://arxiv.org/pdf/math/0205057) computes the orbit count for increasing or decreasing bijections between integer intervals in time polynomial in $k\log N$. The paper’s pairings generate equivalence classes under inverses and composition, as required.

All pairings used in the output are translations between equal-length integer intervals. Reversing a pairing’s orientation of description, shifting indices, and converting half-open intervals to inclusive integer intervals do not change the generated equivalence relation. The auxiliary graphs need not satisfy the original forest or port promises.

Lemma 3 is correct. The added interval chains and singleton edges connect precisely the vertices of $S$ to $z$, possibly joining several original components that meet $S$. An original component disjoint from $S$ remains untouched. Adding $\{v,z\}$ therefore preserves the component count exactly when the component of $v$ meets $S$.

The construction uses only polynomially many pairings and polynomial-length integers. Empty $S$ also behaves correctly: $z$ remains isolated before the final edge is added.

Lemma 4 is correct. Both displayed translation formulas encode the bipartite double cover. Each edge switches sheets. In a forest, every closed walk has even length, so connectivity between the specified lifted vertices detects precisely the parity of the unique simple path. The case of equal specified vertices gives even parity as expected.

4. Degree-two construction

The structure of $F$ is correctly established. Every nonisolated vertex retains its first-choice edge. Its arrow therefore stays within its component of $F$. For a nontrivial component with $n$ vertices, the arrow count gives
$$ n=(n-1)+d, $$
so exactly one edge is mutual first choice.

Maximum degree at most $2$ makes the component a path. After removing the mutual edge, the first-choice arrows point toward the appropriate sink endpoint.

The definition and stability of $J$ are correct. The sink endpoints are paired together; each arm pairs distances $1$ with $2$, then $3$ with $4$, and so forth. Every unselected arm edge has an even-distance endpoint receiving its first choice. Odd-distance terminal vertices are unmatched. This includes arms of length zero or one.

The statement about matched component endpoints is valid: such an endpoint is either a sink endpoint or an even-distance terminal vertex, and receives its first choice.

The extension through $E_0$ is correct. An endpoint of a discarded edge has another neighbor, its first choice. Under the degree bound, it cannot have a second discarded edge. Hence $E_0$ is a matching, and its endpoints are terminal vertices of their $F$-components.

Adding discarded edges only between two unmatched vertices preserves feasibility and cannot create blocking edges in $F$. Every discarded edge left unselected has an endpoint already matched under $J$; that endpoint receives its first choice and rejects the edge.

This proves that $S$ is stable, so Lemma 1 identifies it with the unique stable matching.

The succinct implementation is correct.

All local queries, interval modifications, and orbit-counting calls have polynomial input size. There are polynomially many calls, since $\log_2 D\leq L$. Lemma 2 therefore proves the stated degree-two circuit-construction theorem.

5. Polynomial-space queries for arbitrary branching

The offer recurrence is correct. The induction treats the modification inside the selected child subtree, which is essential. When that child is matched to the root, its descendants receive their standalone subtree matchings. Any descendant that would accept the child is rejected by the child’s preferred new assignment. The other root-child edges are rejected either by the child or by the root.

The resulting stable matching proves the root-partner characterization. Applying it to $T(v\mid u)$ yields the displayed recurrence, including the empty-disjunction case.

The component-size procedure is correct. The cyclic successor permutation has one cycle on the oriented edges of a nontrivial tree. The leaf-insertion argument justifies this assertion. Consequently,
$$ s(v\mid u)=1+\ell/2. $$
The isolated case is separately covered. Storing two oriented edges, a counter, and local-query data uses polynomial space, even when the traversal takes exponential time.

The heavy-child evaluation is correct. Relevant child components are disjoint, so at most one exceeds half the current component size. All recursive calls therefore enter components of at most half that size.

After all other relevant offers are false, the recurrence reduces to complementation of the heavy child’s offer. Iterating this step and recording complementation parity avoids pushing frames along a long heavy chain. Every actual recursive descent halves component size, giving the stated logarithmic stack-depth bound.

Each frame and each component-size calculation uses polynomial space. Evaluating the offers of the queried vertex’s neighbors sequentially proves the proposition. It supplies no polynomial-time guarantee and is not presented as doing so.

6. Branching example and computational check

The branching counterexample is correct. The sole discarded edge is $\{v,u\}$. In the stated matching of $F$, vertex $v$ receives $w$ and vertex $u$ is unmatched, so both prefer $\{v,u\}$. The alternative matching displayed for the full tree is stable: the remaining edges are rejected by $a$, $c$, or $v$ as described.

The seven-cell interval realization preserves the finite example and is compatible with the task’s presentation.

The reported exhaustive check is ancillary and not reproducible from the output. The number $1{,}023$ is consistent with enumerating all endpoint-consistent preference sequences for the stated path sizes. However, no executable code or results artifact is supplied to verify that the comparison was actually performed. This is a minor documentation issue; the mathematical proof does not depend on it.

7. Issues and actionable feedback

Major — the unrestricted target remains unsettled. Sections 4 and 5 establish restricted polynomial time and general polynomial space, respectively. Neither establishes either requested alternative for arbitrary promised presentations.

To resolve USER_TASK, the next write-up must supply either an unrestricted polynomial-time circuit constructor with a proved size and running-time bound, or an $\mathrm{NP}$-hardness reduction under polynomial-time Turing reductions. This requires additional mathematics, not clarification of the existing proof.

Minor — the empirical check lacks verification artifacts. If retained as an independently checkable computational claim, provide the enumeration code and comparison output. Otherwise, omit it. No change to the proof is needed.

The direction is promising because both subsidiary results withstand verification. “Open in this write-up” is justified; the output does not establish a broader claim that the unrestricted problem is open in the literature.

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