# P/NP Debate Game Research Area | Round 11

## Collapse of Common Preservation Structure and Dynamic Bridging: Does the Interface Between Locally Solvable Modules Regenerate Existential Quantifiers?

**Round 11: Collapse of Common Preservation Structure and Dynamic Bridging**

- **Lead Researcher:** Neo.K (Hsu Chuan-Wei)
- **Collaborative Organization:** Aletheia
- **Institution:** EveMissLab (Eno Technology Co., Ltd.)
- **Date:** August 1, 2026
- **Version:** v1.0
- **Research Status:** Round 11 Dual-Hypothesis Rehearsal
- **Prerequisite Document(s):** `10_Round_10_Multiple_Anti-Structure_Cores_and_Heterogeneous_Gluing_Debt.md`
- **Game Stance:** Team Equality and Team Inequality dismantling each other's bridges
- **Document Standard:** Game scores do not represent mathematical evidence; all generalized conclusions require additional proofs

---

## Abstract

Round 10 advanced the research focus from "which good structure a certain problem lacks" to "how multiple locally tractable structures lose their common low-cost structure when glued globally," proposing HGD (Heterogeneous Gluing Debt) and Dynamic Algebra Switching.

This round further formalizes this conflict. Suppose a global constraint problem is decomposed into multiple local modules:

$$
F(B,Y_1,\ldots,Y_m)
=
\bigwedge_{i=1}^{m}F_i(B_i,Y_i),
$$

where $Y_i$ are the private variables of module $i$, and $B_i\subseteq B$ are the boundary variables shared with other modules. Even if each $F_i$ belongs to a local theory solvable in polynomial time, the true global problem can still be written as:

$$
\exists B\;\bigwedge_{i=1}^{m}
\left[\exists Y_i\,F_i(B_i,Y_i)\right].
$$

Thus, we can define the **Boundary Extension Relation** for each module:

$$
\mathcal E_i(B_i)
=
\left\{
 b_i\mid \exists Y_i\,F_i(b_i,Y_i)
\right\}.
$$

Global satisfiability is then precisely equivalent to:

$$
\exists b\in\{0,1\}^{B}
\quad
\forall i,
\quad
b|_{B_i}\in\mathcal E_i.
$$

This reveals the core mechanism of this round: **local existential quantifiers can be individually eliminated, but the global existential quantifier will reappear at the interface.** This document refers to this phenomenon as "Existential Reappearance."

Based on this, Team Equality proposes an enhanced version of Dynamic Algebra Switching: local modules do not need to share the same polymorphism or the same algebra. As long as each module has a polynomial-time solver, and there exists a polynomial-sized, composable, and precisely coordinable boundary summary / bridge protocol between modules, the global problem can still maintain polynomial time. SMT, DPLL(T), Nelson–Oppen theory combination, and the deep integration of SAT/XOR like CDCL(⊕) emerging in 2026 all provide practical precedents that "different reasoning algebras can cooperate via a bridging layer."

Team Inequality points out: the bridge itself may become a new combinatorial core. Nelson–Oppen-style methods require local theory solvers to agree on the equality arrangement of shared/interface variables; relevant theory-combination literature explicitly states that the arrangement space can incur exponential costs in the worst case. More fundamentally, if the bridge framework is sufficient to treat every clause of an arbitrary CNF as a "locally easy module" and can still coordinate all shared variables at a polynomial cost, then the bridge itself is already a general SAT solver. This forms a new "Bridge Universality Trap."

This round does not claim to have proven $P\neq NP$. Its main achievement is transforming the HGD from Round 10 into a precisely unfoldable **interface coordination problem**, and establishing four working objects: Boundary Extension Relation, Existential Reappearance, Polynomial Bridge Principle, and Bridge Universality Trap. The next round will investigate: as the bridge language continuously strengthens, is it inevitable to regenerate an "interface SAT" equivalent to the original SAT, and does there exist an independently characterizable hierarchy among bridge expressiveness, summary size, and coordination cost.

---

# I. The Problem of This Round: If Local Modules Are All Solvable, Why Might the Combination Still Be Hard?

In Round 10, Team Inequality attempted to utilize polymorphism intersection collapse:

$$
\operatorname{Pol}(\Gamma_1)
\cap\cdots\cap
\operatorname{Pol}(\Gamma_m)
$$

which might lose the common operations sufficient to support known tractable algorithms after heterogeneous constraint families are glued together.

Team Equality's response was:

> I do not need to use a single algebra globally at all.

For example:

- Horn blocks use Horn propagation;
- XOR blocks use $\mathbb F_2$ linear algebra;
- 2-SAT blocks use implication graphs;
- difference logic uses graph shortest-path / negative-cycle reasoning;
- arrays, EUF, and linear arithmetic use their respective theory solvers;
- the outermost layer uses SAT/SMT orchestration to decide when to switch.

Such systems are not fantasies in modern SMT. The fundamental spirit of DPLL(T) is to cooperate propositional search with theory-specific decision procedures; Nelson–Oppen theory combination studies how to combine different theory solvers on shared variables into a correct overall decision procedure.

Therefore, what Team Inequality truly needs to answer is no longer:

$$
\text{"Why is there no common polymorphism?"}
$$

but rather:

$$
\boxed{
\text{"Does the bridging between different local algebras inherently bear a new global combinatorial cost?"}
}
$$

---

# II. Common Model: Local Modules and Boundary Variables

Let the global problem be written as:

$$
F
=
\bigwedge_{i=1}^{m}F_i(B_i,Y_i),
$$

satisfying:

1. $Y_i$ are the private variables of module $i$;
2. $Y_i\cap Y_j=\varnothing$ for $i\neq j$;
3. $B_i$ are the interface variables shared by module $i$ with the outside;
4. $B=\bigcup_i B_i$.

Assume each local module $F_i$ has its own polynomial-time decision procedure:

$$
A_i\in P.
$$

But what "locally solvable" truly provides is: given a boundary value $b_i$, we can determine whether there exists a private variable extension:

$$
\operatorname{Ext}_i(b_i)
=
1
\iff
\exists Y_i\,F_i(b_i,Y_i).
$$

Define:

$$
\boxed{
\mathcal E_i
=
\{b_i:\operatorname{Ext}_i(b_i)=1\}
}
$$

as the **Boundary Extension Relation (BER)** of module $i$.

This definition intentionally only records "which interface states can extend into the module's interior," without preserving the entire history of the local solving.

---

# III. Existential Reappearance Lemma

If the private variables $Y_i$ do not overlap with each other, then:

$$
\exists B,Y_1,\ldots,Y_m
\bigwedge_{i=1}^{m}F_i(B_i,Y_i)
$$

is equivalent to:

$$
\exists B
\bigwedge_{i=1}^{m}
\left(\exists Y_iF_i(B_i,Y_i)\right).
$$

Using BER, this can be rewritten as:

$$
\boxed{
\exists B
\bigwedge_{i=1}^{m}
\left[B_i\in\mathcal E_i\right].
}
$$

There are no complexity conclusions here; it is merely a logical equivalence after separating the quantifiers and private variables.

However, it reveals an important structure:

$$
\text{local solving}
\longrightarrow
\text{boundary projection}
\longrightarrow
\text{global coordination}.
$$

Local solvers can individually eliminate:

$$
\exists Y_i,
$$

but globally, there remains:

$$
\exists B.
$$

This document refers to this phenomenon as:

$$
\boxed{
\text{Existential Reappearance}
}
$$

That is:

> Decomposing a global existential problem into multiple tractable modules does not automatically eliminate existentials; the existential quantifier may simply be pushed from inside the modules to the module interfaces.

---

# IV. The First Counterexample: Every Clause is Super Easy

Consider an arbitrary CNF:

$$
F=C_1\land C_2\land\cdots\land C_m.
$$

If we treat each clause $C_i$ as an independent module, then each local problem is extremely easy:

$$
C_i
$$

As long as it is not an empty clause, it is very easy to evaluate individually and very easy to find a satisfying assignment.

Therefore:

$$
\forall i,
\quad
A_i\in P.
$$

One could even say the local cost is almost constant-level.

But all clauses share the same set of variables, and the global condition is:

$$
\exists x_1,\ldots,x_n
\quad
\bigwedge_i C_i(x).
$$

Which is exactly the original SAT.

Thus:

$$
\boxed{
\text{"All modules are in P" itself has almost no global complexity implications.}
}
$$

If a bridge can arbitrarily coordinate clause-level local solvers in polynomial time, then the bridge has already solved SAT.

This is the first important warning of this round:

$$
\text{local tractability}
\neq
\text{compositional tractability}.
$$

---

# V. Team Equality's Move: Polynomial Bridge Principle

Team Equality accepts that the bridge is not free, but proposes a clear sufficient condition.

For each module $F_i$, assume there exists a boundary compiler:

$$
\operatorname{Comp}_i(F_i)
\mapsto
S_i,
$$

where $S_i$ is an exact summary of the BER $\mathcal E_i$, satisfying:

$$
|S_i|\leq\operatorname{poly}(|F|),
$$

$$
T_{\operatorname{Comp}_i}\leq\operatorname{poly}(|F|).
$$

Further assume there exists a bridge algorithm:

$$
\operatorname{Bridge}(S_1,\ldots,S_m)
$$

that can determine in polynomial time whether there exists a common boundary:

$$
\exists b
\quad
\forall i,
\quad
b|_{B_i}\in\mathcal E_i.
$$

Then the overall problem can obviously be solved in polynomial time.

Thus, we obtain a sufficient principle within a finite model:

## Polynomial Bridge Principle (PBP)

If:

1. The number of modules is polynomial;
2. Each local module is polynomially solvable;
3. Each boundary relation can be compiled into a polynomial-sized exact summary in polynomial time;
4. The compatibility / join between summaries can be determined in polynomial time;
5. Witness lifting is also polynomial;

Then the overall problem belongs to $P$.

This is not a deep new theorem, but a cost ledger: it clearly explains what bridge conditions Dynamic Algebra Switching truly requires.

---

# VI. SMT/Theory Combination: Dynamic Bridging Truly Exists

Team Equality can now use mature automated reasoning as empirical cases.

## 6.1 Nelson–Oppen

The core of Nelson–Oppen is not requiring two theories to share the same internal algebra, but rather, when signatures are properly separated and theories satisfy conditions like stable infiniteness, allowing their respective decision procedures to agree on the equality / disequality arrangements of shared variables.

Simplified representation:

$$
T_1\text{-solver}
\quad\leftrightarrow\quad
\text{interface arrangement}
\quad\leftrightarrow\quad
T_2\text{-solver}.
$$

That is:

$$
\text{Different local algebras}
+
\text{Controlled interface coordination}
\Rightarrow
\text{Composable decision procedure}.
$$

This directly supports Dynamic Algebra Switching:

$$
\boxed{
\text{Global tractability does not require all local modules to share the same polymorphism.}
}
$$

## 6.2 DPLL(T)

DPLL(T) goes a step further by combining Boolean SAT search with theory-specific solvers. The SAT core manages propositional branching, while the theory solver is responsible for checking theory consistency and returning theory lemmas / conflicts.

This is a true orchestration:

$$
\text{Boolean reasoning}
\leftrightarrow
\text{theory reasoning}.
$$

## 6.3 CDCL(⊕)

The CDCL(⊕) work at the 2026 SAT Conference provides an example closer to this series: classical CDCL / Resolution can perform very poorly on parity-heavy problems, but by directly incorporating parity equations into the proof language, unit propagation, and conflict learning, one can obtain a correspondence to Res$(\oplus)$, significantly improving performance on Tseitin-like problems in experiments.

This once again supports the proposition brought by the initial video:

$$
\text{Changing mathematical representation / reasoning primitives}
$$

can indeed destroy the difficulties present in the old representation.

---

# VII. Team Inequality's Counterattack: Bridge Arrangement Explosion

Theory combination simultaneously provides weapons for Team Inequality.

Local solvers must agree on the relationships of shared variables. If the shared variables are:

$$
V=\{v_1,\ldots,v_k\},
$$

then a complete equality arrangement essentially establishes equivalence classes over $V$ and specifies the necessary equality / disequality relations.

The number of feasible arrangements can grow rapidly with $k$; calculated by all set partitions, its number is governed by the Bell number $B_k$.

However, this round does **not** deduce from

$$
B_k\text{ is very large}
$$

directly to:

$$
\text{theory combination must be slow}.
$$

Because convexity, equality propagation, care functions, and other structures might avoid enumerating all arrangements.

The truly reliable conclusion is simply:

> The bridge has its own search space, and efficient combination requires additional structure to compress this interface search.

The work of Jovanović–Barrett directly points out that a major cost of traditional combination methods is shared-variable arrangement guessing, and reduces the pairs that truly need attention through equality propagation and care functions.

Therefore:

$$
\boxed{
\text{Bridging can be compressed, but "bridge compression itself" also requires structure.}
}
$$

---

# VIII. Bridge Universality Trap

Now we come to the most important self-dismantling of this round.

Suppose we define an extremely strong bridge framework $\mathfrak B$, which allows:

1. An arbitrary number of local modules;
2. Each module only needs to be individually tractable;
3. Arbitrary shared variables;
4. The bridge determines in polynomial time whether all modules have a globally compatible solution.

Then, taking an arbitrary CNF:

$$
F=\bigwedge_iC_i
$$

and treating each of its clauses as a local module.

The local decision for each clause is trivial, but:

$$
\operatorname{Bridge}(C_1,\ldots,C_m)
$$

If compatibility can be determined in polynomial time, it directly solves SAT in polynomial time.

Thus:

$$
\boxed{
\text{Universal Polynomial Bridge for arbitrary tractable local modules}
\Rightarrow
P=NP.
}
$$

This is not a proof of $P=NP$, but rather says:

> "Locally easy + a completely universal and free bridge" is itself an assumption as strong as a SAT solver.

This document refers to this as:

$$
\boxed{
\text{Bridge Universality Trap}
}
$$

It is the bridge version of the Closure Paradox from Round 6.

---

# IX. Existential Reappearance: The Existential Quantifier Merely Relocates

Rewriting the aforementioned results in quantifier form:

$$
\exists B,Y_1,\ldots,Y_m
\bigwedge_iF_i(B_i,Y_i)
$$

Local solvers can handle:

$$
\exists Y_iF_i(B_i,Y_i),
$$

But ultimately, we still need to handle:

$$
\exists B.
$$

So Dynamic Algebra Switching does not magically eliminate the existential quantifier, but attempts to establish a low-cost representation:

$$
\exists B\;\Phi_{\mathrm{bridge}}(B).
$$

The real question becomes:

$$
\boxed{
\text{Does } \Phi_{\mathrm{bridge}} \text{ possess a lower-cost solvable structure than the original } F \text{?}
}
$$

If it does, Team Equality succeeds.

If the bridge projection / join regenerates a general SAT structure, Team Inequality reclaims the original difficulty.

Therefore, this round proposes:

$$
\boxed{
\text{Existential Reappearance Principle}
}
$$

> Local elimination does not guarantee global elimination; in modular solving, the existential search eliminated locally may reappear in the form of a boundary compatibility search.

Currently, it is a structural principle, not a complexity lower bound theorem.

---

# X. Bridge Coordination Debt (BCD)

To continue the Quotient Debt from Round 9 and the HGD from Round 10, this document defines a provisional resource ledger for the bridge:

$$
\boxed{
\mathbf D_B
=
(
D_{\mathrm{project}},
D_{\mathrm{summary}},
D_{\mathrm{interface}},
D_{\mathrm{arrange}},
D_{\mathrm{propagate}},
D_{\mathrm{join}},
D_{\mathrm{lift}}
)
}
$$

Where:

- $D_{\mathrm{project}}$: The cost of projecting local modules onto the boundary relation;
- $D_{\mathrm{summary}}$: The size/construction cost of exactly representing the BER;
- $D_{\mathrm{interface}}$: The scale of interface variables and shared structures;
- $D_{\mathrm{arrange}}$: The cost of establishing equality / compatibility arrangements;
- $D_{\mathrm{propagate}}$: The cost of propagating information across modules;
- $D_{\mathrm{join}}$: The cost of finding a globally compatible boundary assignment;
- $D_{\mathrm{lift}}$: The cost of lifting the boundary solution back to a complete witness.

It is not claimed here that:

$$
\prod D_j
$$

or:

$$
\sum D_j
$$

possesses any conserved lower bound.

Currently, it is merely a research ledger used to prevent Team Equality from hiding costs behind the word "bridging."

---

# XI. Two Successful Modes of Bridging

Current external theories provide at least two clear successful modes of bridging.

## 11.1 Small Interface / Low Width

If the module interaction graph has a small separator, the possibilities of boundary states can be managed by small summaries.

This aligns with the core spirit of treewidth-based dynamic programming:

$$
\text{Large problem}
\rightarrow
\text{Small separator state}
\rightarrow
\text{Block-by-block join}.
$$

## 11.2 Strong Interface Structure

Even if the number of shared variables is not small, if the theory possesses properties like convexity, stable infiniteness, politeness, or strong equality propagation, it may avoid blindly enumerating all arrangements.

This has mature examples in Nelson–Oppen and its subsequent theory-combination research.

Therefore, true bridge tractability might come from:

$$
\boxed{
\text{small interface}
\quad\text{or}\quad
\text{structured interface}
}
$$

rather than simply:

$$
\text{local modules are easy}.
$$

---

# XII. Team Equality's Upgrade: Dynamic Bridge Portfolio

Team Equality refuses to use only a single bridge.

It proposes:

$$
\boxed{
\text{Dynamic Bridge Portfolio (DBP)}
}
$$

which can dynamically select based on interface characteristics:

$$
B_{\mathrm{eq}},
B_{\oplus},
B_{\mathrm{Horn}},
B_{\mathrm{graph}},
B_{\mathrm{sep}},
B_{\mathrm{SMT}},
B_{\mathrm{learn}},
\ldots
$$

For example:

- equality-heavy interface → congruence closure / Nelson–Oppen;
- XOR-heavy interface → Gaussian / CDCL$(\oplus)$;
- sparse graph interface → separator DP;
- propositional residual → CDCL;
- arithmetic interface → theory propagation;
- repeated conflicts → learned bridge constraints.

Thus, Team Equality's new assertion is not:

$$
\text{There exists a single universal algebra},
$$

but rather:

$$
\boxed{
\text{There exists a uniform polynomial orchestrator capable of continuously selecting and reconstructing bridges.}
}
$$

This is currently the closest constructive version to an "agent / orchestrator" role on the $P=NP$ side.

---

# XIII. Team Inequality Attacks Again: Bridge-of-Bridges Regress

Team Inequality's response is:

If the system is to switch among multiple bridges, it requires a higher-level judgment:

$$
\text{Which bridge should be used now?}
$$

and:

$$
\text{Are the summaries generated by different bridges compatible?}
$$

Thus, this might form:

$$
\text{local solvers}
\rightarrow
\text{bridges}
\rightarrow
\text{bridge orchestrator}.
$$

If the orchestrator itself also uses multiple strategies, there might even emerge:

$$
\text{bridge-of-bridges}.
$$

But this round warns again:

One cannot deduce a super-polynomial lower bound merely from "layers can be added indefinitely."

What truly needs to be proven is:

> Does there exist a solver-independent structure such that any finite-level exact bridge composition must leave behind some compatibility problem that cannot be polynomially compressed?

Currently, there is no such theorem.

Therefore, Bridge-of-Bridges is merely a direction for next steps in research, not a proof.

---

# XIV. Unification with the Previous Ten Rounds

The current research line can be rewritten as:

$$
\text{Existential Search}
\rightarrow
\text{Representation}
\rightarrow
\text{Exact Quotient}
\rightarrow
\text{Local Algebra}
\rightarrow
\text{Heterogeneous Modules}
\rightarrow
\text{Boundary Relations}
\rightarrow
\text{Bridge Coordination}.
$$

The previous rounds kept asking:

$$
\text{Can candidates be quotiented out?}
$$

This round points out that even if local candidates have been successfully quotiented out, there might still be a need for:

$$
\boxed{
\text{Quotient of quotients / Coordination of summaries}
}
$$

Thus, "complexity transfer" now appears in at least three layers:

$$
\text{search debt}
\rightarrow
\text{quotient debt}
\rightarrow
\text{bridge debt}.
$$

But there is still no proof that the sum of these three debts possesses an unvanishable super-polynomial lower bound.

---

# XV. Ruling on the Offense and Defense of This Round

## 15.1 Team Equality Scores

Team Equality proved an important conceptual error:

$$
\text{Lack of common polymorphism}
\not\Rightarrow
\text{Inability to combine polynomially}.
$$

Nelson–Oppen, DPLL(T), SMT, and CDCL$(\oplus)$ all demonstrate that different local reasoning systems can cooperate via specialized bridges.

## 15.2 Team Inequality Scores

Team Inequality successfully formalized HGD into boundary coordination:

$$
\exists B
\bigwedge_i[B_i\in\mathcal E_i].
$$

It also proved that "all local modules are in P" is insufficient to deduce global P, because clause-level decomposition can make all local problems trivial, while the bridge still fully bears the burden of SAT.

Thus, the score for this round:

$$
P=NP:10
\qquad
P\neq NP:10.
$$

The score remains merely a game interface.

---

# XVI. Erroneous Routes Eliminated in This Round

The following arguments must not be used directly:

1. "Different tractable classes have no common polymorphism, therefore $P\neq NP$."
2. "Every local module is in P, therefore the whole should also be in P."
3. "There are many shared-variable arrangements, therefore any combination must enumerate them all."
4. "A certain version of Nelson–Oppen is exponential in the worst case, therefore general SAT must be non-polynomial."
5. "Building an additional layer of orchestrator inevitably makes it harder."
6. "The bridge cost is very high." If the bridge cost is directly defined as the optimal global solving time, it forms a circular argument.
7. Deducing directly from the failure of a finite bridge portfolio that no unknown bridge language exists.

---

# XVII. Formal Achievements of This Round

## Achievement A: Boundary Extension Relation

$$
\mathcal E_i(B_i)
=
\{b_i:\exists Y_iF_i(b_i,Y_i)\}
$$

Provides a precise intermediary layer between local solvers and global coordination.

## Achievement B: Existential Reappearance

$$
\exists B,Y
\bigwedge_iF_i
\equiv
\exists B
\bigwedge_i\exists Y_iF_i.
$$

After local quantifiers are eliminated, the global existential search can reappear at the interface.

## Achievement C: Polynomial Bridge Principle

Local tractability combines into global tractability only when both the boundary summary and the bridge join can be processed in polynomial time.

## Achievement D: Bridge Universality Trap

If a bridge framework can unconditionally and polynomially combine arbitrary tractable local constraints, then clause decomposition directly turns it into a general SAT solver.

## Achievement E: Bridge Coordination Debt

Establishing:

$$
\mathbf D_B
$$

as a unified ledger for subsequently tracking projection, summary, interface, arrangement, propagation, join, and lifting.

---

# XVIII. Gateway to Round 12: Bridge Language Hierarchy

The real question left by this round is:

$$
\boxed{
\text{How expressive can a bridge actually be without reverting back into general SAT?}
}
$$

Tentative topic for Round 12:

## Interface Language Hierarchy and Recursive SAT: The Stronger the Bridge, the Closer It Gets to Regenerating the Original Problem?

Preparing to establish a bridge language hierarchy:

$$
\mathcal B_0
\subseteq
\mathcal B_1
\subseteq
\cdots
\subseteq
\mathcal B_k
\subseteq\cdots
$$

For example:

- $\mathcal B_0$: Simple equality / disequality;
- $\mathcal B_1$: Implication / 2-SAT relations;
- $\mathcal B_2$: Affine / XOR relations;
- $\mathcal B_3$: Horn / bounded-width summaries;
- $\mathcal B_4$: Knowledge-compiled boundary circuits;
- Higher-order: Mixed / learnable bridge relations.

Core controversy:

$$
\text{bridge expressiveness}\uparrow
$$

Is it accompanied by:

$$
\text{bridge coordination complexity}\uparrow,
$$

and does there exist a non-circular critical point:

$$
\boxed{
\text{Once the bridge is sufficient to losslessly represent the boundary relations of general SAT, the bridge itself reverts to SAT.}
}
$$

---

# XIX. Historical Dependencies

This round directly depends on:

1. `07_Round_7_Battle_for_Algebraic_Invariants_and_Algorithmic_Algebraic_Bridges.md`
2. `08_Round_8_Stress_Testing_Algorithmic_Algebraic_Bridges_and_Exact_Quotient_Structures.md`
3. `09_Round_9_Searching_for_the_Blossom_of_SAT_and_Quotient_Debt.md`
4. `10_Round_10_Multiple_Anti-Structure_Cores_and_Heterogeneous_Gluing_Debt.md`

Conceptual dependencies:

$$
\text{polymorphism}
\rightarrow
\text{exact quotient}
\rightarrow
\text{heterogeneous gluing}
\rightarrow
\text{boundary coordination}.
$$

---

# XX. External Theoretical References

1. Greg Nelson and Derek C. Oppen, **Simplification by Cooperating Decision Procedures**, 1979.
2. David Monniaux, **A Survey of Satisfiability Modulo Theory**, 2016.
3. Dejan Jovanović and Clark Barrett, **Being Careful about Theory Combination**, *Formal Methods in System Design*, 2013.
4. Ying Sheng, Yoni Zohar, Christophe Ringeissen, Andrew Reynolds, Clark Barrett, Cesare Tinelli, **Politeness and Stable Infiniteness: Stronger Together**, CADE 2021; and the subsequent 2023 Journal of Automated Reasoning version.
5. Martin C. Cooper and Stanislav Živný, **Hybrid tractability of soft constraint problems**, 2010.
6. David A. Cohen, Martin C. Cooper, Páidí Creed, András Z. Salamon, **The tractability of CSP classes defined by forbidden patterns**, 2011.
7. **Extending CDCL to Disjunctions of Parity Equations**, SAT 2026; used to observe how a parity-aware bridge / proof language alters reasoning behavior on Tseitin-like problems.

---

## Ruling of This Round

$$
\boxed{
\text{Dynamic Algebra Switching is real; but the bridge of Algebra Switching must also be computed.}
}
$$

$$
\boxed{
\text{Local existential quantifier elimination does not equal global existential quantifier disappearance; it may simply reappear on the boundary.}
}
$$

The most worthwhile question to pursue currently is no longer:

$$
\text{"Is there a common algebra?"}
$$

but rather:

$$
\boxed{
\text{"Can the exact summaries of different algebras always be coordinated at a polynomial cost?"}
}
$$

This will lead directly into Round 12.