# P/NP Debate Game Research Area | Round 7

## The Battle for Algebraic Invariants: Do All Tractable Problems Have a "Composable Solution Structure"?

**Round 07: Algebraic Invariants and the Algorithm-to-Algebra Bridge**

- **Lead Researcher:** Neo.K (Hsu Chuan-Wei)
- **Collaborative Organization:** Aletheia
- **Institution:** EveMissLab (Yiyannuo Technology Co., Ltd.)
- **Date:** August 1, 2026
- **Version:** v1.0
- **Research Status:** Round 7 Dual-Hypothesis Rehearsal
- **Prerequisite Document(s):** `00`–`06`
- **Game Stance:** The Equals Team and Not-Equals Team tearing down each other's arguments
- **Document Standard:** Formal research record; game scores hold no evidentiary weight

---

## Abstract

Round 6 established the "representation closure paradox": if arbitrary polynomial-time representation transformations are allowed, then "polynomial-time reducible to a tractable normal form" is almost synonymous with the original problem being in $P$; if representation transformations are restricted too much, the resulting lower bounds can only constrain restricted models. Therefore, Round 7 no longer pursues representations themselves, but turns to studying **algebraic structures preserved under a large class of natural transformations**.

Finite-domain Constraint Satisfaction Problems (CSPs) provide a very strong success story. For a fixed constraint language $\Gamma$, its polymorphism clone

$$
\operatorname{Pol}(\Gamma)
$$

consists of all operations that can coordinate-wise compose multiple valid tuples such that the result still preserves every relation $R\in\Gamma$. Tractable families in the Boolean Schaefer class, such as Horn, dual-Horn, bijunctive, and affine, possess non-trivial preserving operations like conjunction, disjunction, majority, and affine/minority, respectively; the more general finite-domain CSP dichotomy relies on weak near-unanimity / Taylor-type polymorphisms as one of its core algebraic structures. The independent works of Zhuk and Bulatov completed the finite-domain CSP dichotomy; subsequent works further simplified and unified this algebraic theory.

This looks very much like the "cross-syntax invariant" the Not-Equals Team has been searching for: tractability does not arise from the formula looking simple, but from the solution relation possessing a composable closure structure.

However, the Equals Team immediately points out a fatal limitation: the formal conclusion for the hard side of the CSP dichotomy is **NP-complete**, not unconditionally "not in $P$". If we assume $P=NP$, these NP-complete CSPs lacking tractable polymorphisms would still have polynomial-time algorithms. Thus, polymorphisms can unconditionally prove that certain languages **have** polynomial-time algorithms, and can also prove that other languages exhibit NP-completeness, but they cannot yet serve as a "necessary condition for the existence of any polynomial-time algorithm", otherwise $P/NP$ would have already been implicitly resolved.

This round thus arrives at a new core question:

> **Algorithm-to-Algebra Bridge Problem: Does any exact polynomial-time solver necessarily induce some non-trivial, independently definable solution-space composition structure?**

If the answer is yes, there is a chance to pull "arbitrary algorithms" back into the realm of researchable algebraic invariants; if the answer is no, the Equals Team gains an important escape route: polynomial-time algorithms might exist without needing to exhibit any non-trivial polymorphism for the original constraint language.

---

# I. Common Model: Constraint Language and Polymorphism

Let the finite domain be:

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

A constraint language is a finite set of relations:

$$
\Gamma=\{R_1,\ldots,R_m\},
$$

where each:

$$
R_i\subseteq D^{r_i}.
$$

An instance of $\operatorname{CSP}(\Gamma)$ consists of a set of variables and several $R_i$ constraints; the problem is to determine whether there exists a global assignment satisfying all constraints simultaneously.

Let $f:D^k\rightarrow D$ be a $k$-ary operation. If for any relation $R\in\Gamma$ and any $k$ tuples:

$$
\mathbf a^{(1)},\ldots,\mathbf a^{(k)}\in R,
$$

applying $f$ coordinate-wise still yields:

$$
f\left(\mathbf a^{(1)},\ldots,\mathbf a^{(k)}\right)\in R,
$$

then $f$ is called a polymorphism of $R$; if it preserves all relations in $\Gamma$, then:

$$
f\in\operatorname{Pol}(\Gamma).
$$

Therefore:

$$
\operatorname{Pol}(\Gamma)
$$

is not a syntactic feature of a specific formula, but a **family of solution-structure closure operations** for the entire constraint language.

All projection operations are always polymorphisms, so what truly matters is whether non-trivial operations exist and what identities they satisfy.

---

# II. Four Classic "Solution Synthesizers" in the Boolean World

The Boolean Schaefer class provides the most intuitive testing ground.

## 2.1 Horn: AND Composition

Horn relations have conjunction closure. If:

$$
\mathbf a,\mathbf b\in R,
$$

then the coordinate-wise AND:

$$
\mathbf a\wedge\mathbf b\in R.
$$

Thus, two valid solutions can be composed via:

$$
f_{\wedge}(x,y)=x\wedge y
$$

into another valid solution.

This is a very strong solution-space closure.

## 2.2 Dual-Horn: OR Composition

Conversely, dual-Horn relations are preserved by:

$$
f_{\vee}(x,y)=x\vee y
$$

If two tuples are valid, their coordinate-wise OR remains valid.

## 2.3 Bijunctive / 2-SAT: Majority Composition

For bijunctive relations, a core polymorphism is the majority operation:

$$
\operatorname{maj}(x,y,z)
$$

which takes the majority value among three Boolean values.

Therefore:

$$
\mathbf a,\mathbf b,\mathbf c\in R
$$

can be composed into:

$$
\operatorname{maj}(\mathbf a,\mathbf b,\mathbf c)\in R.
$$

## 2.4 Affine: XOR / Minority Composition

Affine relations can be described by linear/affine structures, and their solution sets form affine spaces over $\mathbb F_2$. A typical ternary preserving operation is:

$$
m(x,y,z)=x\oplus y\oplus z.
$$

Thus, three solutions can generate another solution via affine combination.

This perfectly echoes the Tseitin reversal from Round 4: certain parity structures that are extremely difficult in resolution possess extremely strong algebraic closure and Gaussian elimination once they enter $\mathbb F_2$.

---

# III. The Not-Equals Team's First Card: Tractability Might Stem from "Solution Composability"

For the past six rounds, the Not-Equals Team has been searching for:

$$
\text{What structure does not disappear under syntactic rewriting?}
$$

Polymorphisms provide a very elegant candidate answer:

$$
\boxed{
\text{Do not look at how the formula is written, but whether valid tuples can be stably composed by some non-trivial operations.}
}
$$

This is closer to the semantic level than:

$$
\text{CNF size, decision tree size, fixed variable ordering}
$$

The Not-Equals Team therefore proposes:

> **Solution Aggregation Hypothesis:** Broad polynomial-time tractability is usually accompanied by some low-cost, non-trivial, and repeatedly composable solution-space operation, allowing local information to be converged, averaged, intersected, projected, or linearly combined without destroying validity.

Formally, if there exists a family of operations:

$$
\mathcal F\subseteq\operatorname{Pol}(\Gamma)
$$

and $\mathcal F$ satisfies sufficiently strong algebraic identities such that local consistency, absorption, decomposition, or linearization can be completed within polynomial resources, then:

$$
\operatorname{CSP}(\Gamma)\in P.
$$

This is highly consistent with the Boolean Schaefer class and the algebraic approach to finite-domain CSPs.

---

# IV. General Finite-Domain CSPs: Not a Single Operation, but Identity Types

Over general finite domains, what truly matters is often not specifying a particular AND, OR, or majority, but whether:

$$
\operatorname{Pol}(\Gamma)
$$

contains operations satisfying certain classes of identities.

For example, weak near-unanimity (WNU) operations have the form:

$$
f(y,x,x,\ldots,x)
=
f(x,y,x,\ldots,x)
=
\cdots
=
f(x,x,\ldots,y),
$$

and typically require idempotence:

$$
f(x,\ldots,x)=x.
$$

The algebraic theory of the finite-domain CSP dichotomy shows that such Taylor/WNU structures are closely related to positive algorithms for polynomial-time tractability; the side lacking corresponding structures can establish NP-completeness.

Therefore, the Not-Equals Team decides to no longer just preserve "whether a certain operation exists", but to establish:

$$
\boxed{
\operatorname{APS}(\Gamma)
=
\text{Algebraic Preservation Spectrum}
}
$$

namely the **Algebraic Preservation Spectrum**: recording which operation identities, closure properties, and composition classes $\operatorname{Pol}(\Gamma)$ satisfies.

This spectrum is more robust than a single function because the polymorphism clone itself is closed under composition.

---

# V. Why is this More Promising than "Representation Size"?

For finite constraint languages, there is a profound Galois correspondence between polymorphisms and primitive-positive definability: the relations a language can define through existential quantifiers, variable sharing, and conjunctions correspond closely to the polymorphisms that preserve that language.

Therefore:

$$
\text{pp-definability}
\quad\leftrightarrow\quad
\text{polymorphism preservation}
$$

provides a rare example of a cross-representation invariant.

If two constraint languages can pp-define each other using lower-order relations, their polymorphism structures will be strongly constrained; this makes it difficult for "changing to another CNF formulation" to create algebraic closures out of thin air.

This is exactly what Round 6 was looking for but failed to find:

$$
\boxed{
\text{A natural transformation closure that is not an arbitrary P-time transformation, yet much broader than a single syntactic representation.}
}
$$

---

# VI. The Equals Team's Counterkill: NP-complete is Not "Not in P"

The Equals Team catches the most important logical loophole this round.

The hard side of the finite-domain CSP dichotomy tells us:

$$
\text{Lack of appropriate polymorphism}
\Rightarrow
\operatorname{CSP}(\Gamma)\text{ is NP-complete}.
$$

But:

$$
\text{NP-complete}
\not\Rightarrow
\text{not in }P
$$

unless it is already known that:

$$
P\neq NP.
$$

If we assume:

$$
P=NP,
$$

then all NP-complete CSPs still possess polynomial-time algorithms, even if they completely lack the polymorphism identities of the current tractable side.

So the Equals Team lands a very heavy counterattack:

$$
\boxed{
\text{Polymorphisms can characterize known structural tractability,}
}
$$

$$
\boxed{
\text{but cannot yet prove to be a necessary condition for "any possible P algorithm".}
}
$$

Otherwise, we would have actually secretly proven:

$$
P\neq NP.
$$

---

# VII. The Equals Team's Second Card: Algorithms Do Not Have to Preserve Solution Sets

What polymorphisms do is:

$$
\text{solution tuple}
\rightarrow
\text{solution tuple}.
$$

But the task of a general decision algorithm is only:

$$
I
\mapsto
\{0,1\}.
$$

It can absolutely:

- Transform the original instance into another mathematical object;
- Generate a large number of invalid assignments in the intermediate steps;
- Use determinants, spectral quantities, generating functions, or other global invariants;
- Never explicitly construct two solutions and then compose them;
- Destroy all intuitive closures of the original constraint language, yet still compute the correct YES/NO in the end.

Therefore:

$$
\boxed{
\text{solution-space symmetry}
\neq
\text{arbitrary algorithm symmetry}.
}
$$

This is the most critical model boundary of this round.

---

# VIII. Thought Experiment 1: What if SAT Suddenly Had a Completely Unfamiliar P Algorithm?

Suppose tomorrow someone presents:

$$
A_{\mathrm{SAT}}(\varphi)
$$

with a time complexity of:

$$
O(n^{17}),
$$

but its method completely does not utilize:

- Horn closure;
- majority;
- affine structure;
- WNU;
- bounded width;
- Any tractability identities recognizable by current CSP algebra.

It merely computes some invariant:

$$
J(\Psi(\varphi)),
$$

on a new high-dimensional mathematical object:

$$
\Psi(\varphi)
$$

and satisfies:

$$
J(\Psi(\varphi))=0
\iff
\varphi\text{ is UNSAT}.
$$

If this were true, the original constraint language's:

$$
\operatorname{Pol}(\Gamma)
$$

would not need to change at all.

That is:

$$
\text{The language's algebraic preservation spectrum}
$$

and:

$$
\text{whether an external P-time algorithm exists}
$$

are logically on different levels.

Therefore, APS can currently only serve as **algorithmic structural evidence**, not as a complete criterion for the existence of general algorithms.

---

# IX. The Not-Equals Team Upgrades: Forcing "Algorithms" Back to "Algebra"

If the Not-Equals Team wants to continue down this path, they must build a true bridge:

$$
\boxed{
\text{Polynomial-Time Algorithm}
\Longrightarrow
\text{Nontrivial Algebraic Structure}.
}
$$

Thus, they propose the next core candidate conjecture.

## 9.1 Induced Aggregation Conjecture (IAC)

For a sufficiently broad and naturally defined constraint family, if there exists a uniform deterministic polynomial-time exact solver:

$$
A\in P,
$$

then there exists some low-cost operation family induced by $A$'s computational behavior, self-reduction, canonicalization, or product construction:

$$
\mathcal F_A,
$$

such that $\mathcal F_A$ possesses non-trivial preservation properties for the solution semantics of the problem family.

The formal goal is not to directly require:

$$
\mathcal F_A\subseteq\operatorname{Pol}(\Gamma),
$$

because this might be too strong; instead, it seeks a larger "algorithm-induced preservation structure":

$$
\operatorname{AIP}(A,\Gamma)
$$

where AIP is tentatively called:

$$
\boxed{
\text{Algorithm-Induced Preservation Structure}
}
$$

namely the **Algorithm-Induced Preservation Structure**.

---

# X. Why Might Self-Reducibility Provide a Bridge?

SAT possesses classic self-reducibility.

If we have a decision oracle/algorithm:

$$
A(\varphi)\in\{0,1\},
$$

we can sequentially fix variables:

$$
\varphi[x_1=0],
\qquad
\varphi[x_1=1],
$$

and construct a satisfying assignment using a polynomial number of decision calls.

Therefore:

$$
\text{SAT decision in }P
\Rightarrow
\text{SAT search in }P.
$$

Furthermore, one can define a canonical selector, such as the lexicographically least satisfying assignment:

$$
s(\varphi)
=
\min_{\mathrm{lex}}\{w:V(\varphi,w)=1\}.
$$

If SAT is in $P$, then $s(\varphi)$ can also be constructed in polynomial time.

This allows the Not-Equals Team to see a possible bridge:

$$
\text{decision algorithm}
\rightarrow
\text{canonical solution selector}
\rightarrow
\text{solution-space operation?}
$$

But the last arrow has not yet been established.

---

# XI. The Equals Team's Third Counterattack: A Selector is Not a Polymorphism

The Equals Team points out that a canonical selector:

$$
s(I)
$$

only selects one solution from **a single instance** at a time.

Polymorphisms, however, require:

$$
\mathbf a^{(1)},\ldots,\mathbf a^{(k)}\in R
\Rightarrow
f(\mathbf a^{(1)},\ldots,\mathbf a^{(k)})\in R.
$$

The two types are completely different.

Even if:

$$
P=NP,
$$

we only obtain "a solution can be found quickly", which does not mean "there exists a fixed coordinate-wise closure among multiple solutions".

For example, a solution set might have an extremely irregular geometric structure, but a solver could still directly find a point within it via some global certificate.

Therefore:

$$
\text{fast search}
\not\Rightarrow
\text{coordinate-wise algebraic closure}.
$$

For IAC to hold, it must allow for induced operations that are more general than classical polymorphisms.

---

# XII. The Not-Equals Team Pivots: Perhaps the True Invariant is Not "Solution Closure", but "Compressible Composition"

The most important conceptual revision of this round appears here.

Original polymorphisms require:

$$
\text{Solution}+\text{Solution}
\rightarrow
\text{Solution}.
$$

But what general efficient algorithms truly need might just be:

$$
\boxed{
\text{A large number of local possibilities}
\rightarrow
\text{A low-dimensional, iteratively updatable sufficient statistic}.
}
$$

So the object of study is relaxed to:

## 12.1 Polynomial Aggregation Structure (PAS)

For a local/partial information set $X_I$ of an instance $I$, if there exists a summary space:

$$
S_I,
$$

and a composition operation:

$$
\star:S_I\times S_I\rightarrow S_I,
$$

satisfying:

1. Each piece of local information can be polynomially encoded as an element of $S_I$;
2. The summary size is $\operatorname{poly}(|I|)$;
3. $\star$ can be computed in polynomial time;
4. Repeated aggregation still retains sufficient information needed to determine satisfiability;
5. The final summary can be decoded into YES/NO in polynomial time.

then it is called a polynomial aggregation structure.

Horn's meet, 2-SAT's implication/SCC structure, affine's linear subspaces, and bounded-treewidth DP's bag tables can all be viewed as different forms of PAS candidates.

Note: PAS is much broader than polymorphisms because the summary does not have to be a satisfying assignment.

---

# XIII. The Equals Team's Fourth Counterattack: Is PAS Too Broad, Repeating Round 6?

The Equals Team immediately points out:

If the PAS definition allows arbitrary polynomial-size summaries and polynomial-time combine/decode, then for any:

$$
L\in P
$$

one can simply let the summary be:

$$
S_I=\{A(I)\},
$$

or treat the entire polynomial-time computation history as the summary.

Then:

$$
\text{Existence of PAS}
\Longleftrightarrow
L\in P,
$$

repeating the closure paradox of Round 6.

So if PAS is to become a true invariant, it must have **independent structural restrictions**, such as:

- Local composability;
- Bounded arity;
- Associative / commutative / idempotent identities;
- Naturality with respect to instance decomposition;
- Not allowing the summary to directly equal the entire solver state;
- Being definable independently of the running time to be proven.

Thus, this round confirms once again:

$$
\boxed{
\text{A "structure" that is too general is synonymous with }P\text{; a structure that is too narrow only covers known algorithms.}
}
$$

---

# XIV. Candidate Invariant Scorecard

| Candidate | Semantic Nature | Cross-Representation Robustness | Derives P Algorithm | Unconditionally Excludes P | Current Verdict |
|---|---:|---:|---:|---:|---|
| Horn $\wedge$ closure | High | High (for languages) | Yes | No | Successful tractability structure |
| Bijunctive majority | High | High (for languages) | Yes | No | Successful tractability structure |
| Affine minority/XOR | High | High (for languages) | Yes | No | Successful tractability structure |
| WNU/Taylor polymorphism | High | High (finite CSPs) | Yes | Hard side only NPC | Strong reference |
| $\operatorname{APS}(\Gamma)$ | High | High (pp world) | Partial | No | Retained |
| Canonical solution selector | High | Medium | Yes, if decision in P | No | Bridging component |
| IAC | Unknown | Target High | Potentially very strong if true | Unproven | Core conjecture |
| unrestricted PAS | High | High | Yes | Circular | Eliminated overly broad version |
| structured PAS | TBD | TBD | Possible | TBD | Next stage candidate |

---

# XV. The Most Important Logical Boundary of This Round

The following two statements must be strictly separated.

## Known Proposition

$$
\text{Some nontrivial polymorphism}
\Rightarrow
\text{Existence of a polynomial-time algorithm}.
$$

This holds in a large number of CSP tractable classes and is an important foundation of known algorithmic theory.

## Proposition We Do Not Yet Possess

$$
\text{Existence of a polynomial-time algorithm}
\Rightarrow
\text{Must imply some nontrivial polymorphism / preservation structure}.
$$

If the second statement holds for sufficiently general NP-complete CSPs, and the hard templates can be proven to lack this structure, it would be very close to, or directly lead to:

$$
P\neq NP.
$$

Therefore, the second statement itself is an extremely high-difficulty core, and we cannot pretend it is a conclusion already provided by the CSP dichotomy.

---

# XVI. Barrier Review

## 16.1 Relativization

Polymorphisms are algebraic properties of the input relations, not typical oracle-black-box methods; thus, this line of reasoning does not automatically fall into the simplest relativization framework just because it "looks algebraic".

However, if the proof of the Algorithm-to-Algebra bridge relies only on input-output behavior that an oracle can preserve, it might still relativize.

**Status:** Not cleared, requires dedicated oracle testing.

## 16.2 Natural Proofs

If AIP/PAS can be efficiently identified in the future, holds for a sufficiently large set of Boolean functions, and is simultaneously used to rule out polynomial circuits, it might encounter natural proofs-type barriers.

**Status:** Risk unknown.

## 16.3 Algebrization

This round explicitly uses universal algebra. This does not mean it automatically falls into the Aaronson–Wigderson algebrization barrier; the meaning of "algebra" is different in the two contexts. But any proof that ultimately transforms into arithmetization + oracle extension still needs testing.

**Status:** Cannot be misjudged due to name similarity, requires further investigation later.

## 16.4 Circularity

This round has eliminated unrestricted PAS because it can directly package the entire P-time solver into the summary.

**Status:** Discovered and blocked one type of circular definition.

---

# XVII. Erroneous Routes Eliminated This Round

The following can no longer be directly claimed as arguments for $P\neq NP$:

1. "General 3-SAT lacks Horn/majority/affine closure, so it is not in P";
2. "The CSP dichotomy says the hard side is NP-complete, so the hard side is not P";
3. "All fast algorithms must produce classical polymorphisms on the original solution set";
4. "If SAT is in P, one can definitely construct a coordinate-wise closure directly from a lexicographic selector";
5. "As long as one defines a summary that can aggregate all information, a new invariant is obtained";
6. "Universal algebra has already classified all possible SAT algorithms".

---

# XVIII. Formal Results of This Round

## 18.1 Not-Equals Team Score: Found a Truly Successful Example of a Cross-Syntax Tractability Invariant

Polymorphism clones and operation identities are the first batch of structural tools in the entire game so far that truly transcend a large number of surface representations and can unconditionally derive polynomial-time algorithms.

Therefore:

$$
P\neq NP\text{ Team obtains a high-quality research template.}
$$

## 18.2 Equals Team Score: Proved This Template Has Not Yet Blocked Unknown Algorithms

NP-complete does not equal an unconditional super-polynomial lower bound. If $P=NP$, languages without Schaefer/Taylor tractable polymorphisms could still be solved by some unknown P algorithm.

Therefore:

$$
P=NP\text{ Team secures the "external algorithm escape" channel.}
$$

## 18.3 The New Core Bridge Problem

What is truly needed is no longer:

$$
\text{Finding a beautiful polymorphism}.
$$

But rather:

$$
\boxed{
A\in P
\stackrel{?}{\Longrightarrow}
\text{Some independently characterizable nontrivial induced structure}.
}
$$

This is:

$$
\boxed{
\text{Algorithm-to-Algebra Bridge Problem}
}
$$

---

# XIX. Gateway to Round 8: Conversely Constructing a World That is "Easy Despite Lacking Explicit Closures"

Tentative topic for Round 8:

## Algorithm-Algebra Bridge Stress Test: Can We Find P Problems Whose Tractability Does Not Stem from Any Explicit Solution Closure?

Team Tasks:

### The Equals Team

Find/construct P-time problem families where:

- The solution space appears to have no obvious Horn/majority/affine closure;
- Natural polymorphisms are very weak;
- But there exist global transform, spectral, determinantal, matching, flow, dynamic programming, or other highly efficient algorithms.

The goal is to shatter:

$$
\text{fast algorithm}\Rightarrow\text{classical solution polymorphism}.
$$

### The Not-Equals Team

Prove for these examples one by one: although there is no classical polymorphism, the algorithm still implies some more general aggregation/decomposition invariant.

If a common structure can be successfully extracted every time, it begins to approach a non-circular version of AIP/PAS.

---

# XX. External Verification Record (2026-08-01)

This round re-verified the following research lines:

1. Dmitriy Zhuk, *A Proof of the CSP Dichotomy Conjecture* (2017): Provides a polynomial-time algorithm for finite-domain CSPs with weak near-unanimity polymorphisms, completing one proof route of the dichotomy.
2. Barto, Brady, Bulatov, Kozik, Zhuk, *Unifying the Three Algebraic Approaches to the CSP via Minimal Taylor Algebras* (2021): Unifies the three algebraic routes for finite CSPs by absorption, Bulatov, and Zhuk.
3. Dmitriy Zhuk, *A simplified proof of the CSP Dichotomy Conjecture and XY-symmetric operations* (2024): Re-simplifies the finite CSP dichotomy using methods like strong subalgebras and linear congruences, and provides new characterizations related to symmetric polymorphisms on two-element sets.
4. Boolean clone / Post lattice related literature: Schaefer tractable Boolean constraint languages can be formulated through closure operations such as constants, majority, conjunction, disjunction, and affine/minority.

Note: Some literature uses idiomatic phrasing like "tractable iff" in their abstracts; in the context of the P/NP debate, this research strictly distinguishes between:

$$
\text{Positively providing a P algorithm}
$$

and:

$$
\text{Providing NP-completeness for the hard side}.
$$

The latter should not be reinterpreted as "unconditionally not in P" without first knowing that $P\neq NP$.

---

# XXI. Round Verdict

Round Score:

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

Reasoning:

- The Not-Equals Team: Obtained the tractability template that currently looks most like a true cross-representation invariant—polymorphisms / algebraic identities;
- The Equals Team: Successfully proved that this is still insufficient to block a completely external, completely unfamiliar P-time SAT algorithm.

What this round ultimately leaves behind is not an answer, but a more precise bridge:

$$
\boxed{
\text{If it can be proven that all P-time exact solvers necessarily induce some non-trivial preservation/aggregation structure,}
}
$$

$$
\boxed{
\text{then algebraic methods might truly be upgraded from tractability classification to a }P/NP\text{ separation tool.}
}
$$

Currently, this bridge has not yet been built.