# P/NP Debate Game Research Area | Round 02

## The Battle for a Cross-Representation Invariant: After the Collapse of the Existential Quantifier, What Must Remain?

**Round 02: The Battle for a Cross-Representation Invariant**

- **Lead Researcher:** Neo.K (Hsu Chuan-Wei)
- **Collaborative Compiler:** Aletheia
- **Institution:** EveMissLab (Yiyannuo Technology Co., Ltd.)
- **Date:** August 1, 2026
- **Version:** v1.0
- **Research Status:** Round 02 Dual-Hypothesis Rehearsal
- **Prerequisite Documents:**
  - `00_Mathematical_Construct_State_Machine_Middleware_v1.0.md`
  - `01_Round_01_Existential_Quantifier_State_Collapse.md`
- **Game Attitude:** The Equals Team and the Not-Equals Team tearing down each other's arguments
- **Document Standard:** All conclusions are recorded according to formal research specifications; jokes do not replace proofs

---

## Abstract

Round 01 reformulated the traditional $P/NP$ problem as: given a polynomial-time verifier

$$
V(x,w)\in\{0,1\},
$$

does there exist a unified, exact mathematical state machine, with all necessary resources polynomially bounded, capable of computing the existential aggregation function

$$
\operatorname{EX}_V(x)
=
\bigvee_w V(x,w)?
$$

Round 02 no longer directly discusses "whether the search tree is large," but further asks: if different algorithms can arbitrarily change representations, decomposition methods, variable orderings, algebraic languages, and state encodings, does there exist a **cross-representation invariant** that any deterministic solver must preserve or process, regardless of how the problem is rewritten?

The Not-Equals Team proposes the first candidate: **residual distinguishable load**. For the residual functions generated after partial variables of a Boolean function or SAT formula are assigned, they are classified according to semantic equivalence relations; if a large number of mutually distinguishable residual functions exist on a certain computational cut, then any system that only summarizes read information with finite states, and still needs to accurately determine the answer in the future, must possess sufficiently many distinct states.

The Equals Team points out: the number of residual functions only forms a reliable lower bound under a fixed variable ordering, a fixed cut, and a fixed state summarization mode. General polynomial-time algorithms can rearrange variables, revisit inputs, use global algebraic summaries, introduce auxiliary variables, switch proof systems, or even completely avoid the selected cut. Therefore, local distinguishability is not yet an invariant that holds across all algorithms.

The main achievement of this round is not finding the ultimate invariant, but establishing a set of "candidate invariant qualification tests": semanticity, cross-representation robustness, non-circularity, existential quantifier sensitivity, model coverage, and barrier compatibility. Residual distinguishability passes the semanticity and local lower bound tests, but fails the general model coverage test; it is retained as the first component for constructing composite invariants in the future.

---

# I. Round 01 Results and Round 02 Rules

Round 01 established the common contested object:

$$
\mathcal C_{\exists},
$$

namely, the existential quantifier compressor. The Equals Team needs to construct a polynomially resource-bounded $\mathcal C_{\exists}$; the Not-Equals Team needs to prove that any exact compressor grows super-polynomially in at least one necessary resource.

However, Round 01 left a fatal question:

> Even if a certain search tree, decision graph, elimination ordering, or algebraic representation explodes, is it possible for another representation to compress it?

Therefore, Round 02 stipulates:

1. The size of a specific data structure must not be directly referred to as the complexity of the problem itself;
2. "Not yet having found other representations" must not be treated as the non-existence of other representations;
3. One must not only calculate runtime while ignoring description, construction, memory, and precision;
4. A candidate invariant must first prove that it is not just another name for an algorithm;
5. Every candidate must undergo the Equals Team's "rewrite escape test."

---

# II. What Qualifies as a Cross-Representation Invariant?

Let $f_n:\{0,1\}^n\rightarrow\{0,1\}$ be a family of Boolean functions. Let

$$
\mathcal R(f_n)
$$

denote all finite representations and state machines that can exactly express or compute $f_n$, including programs, circuits, graphs, algebraic expressions, decision graphs, proof systems, and other efficiently simulable structures.

For a candidate quantity

$$
\mathcal I(f_n)
$$

to become a cross-representation invariant supporting $P\neq NP$, it must satisfy at least the following qualifications.

## 2.1 Semanticity

If two representations compute the same function:

$$
R_1\equiv R_2,
$$

then the candidate invariant should not change arbitrarily merely due to syntactic differences.

The ideal situation is:

$$
\mathcal I(R_1)=\mathcal I(R_2)=\mathcal I(f_n).
$$

If exact equality is impossible, there must at least exist a controllable polynomial relationship.

## 2.2 Cross-Representation Robustness

If one representation can be polynomially transformed into another:

$$
R_1\xrightarrow{\operatorname{poly}}R_2,
$$

then the invariant cannot unconditionally disappear after the transformation; otherwise, it is merely a local size metric of a certain language.

## 2.3 Non-Circularity

The following definition has no proof value:

$$
\mathcal I(f_n)
=
\min_{A\text{ computes }f_n}T_A(n).
$$

Because to prove

$$
\mathcal I(f_n)\notin\operatorname{poly}(n)
$$

is equivalent to re-declaring the intent to prove the original problem.

A useful invariant must be independently characterizable by more fundamental combinatorial, algebraic, geometric, information-theoretic, or topological properties.

## 2.4 Existential Quantifier Sensitivity

It must be able to distinguish between:

$$
V(x,w)
$$

being easy to verify, and:

$$
\bigvee_w V(x,w)
$$

its global aggregation.

If the candidate quantity is already huge for the verifier itself, it cannot explain the difference between $P$ and $NP$.

## 2.5 General Model Relevance

The candidate quantity cannot be restricted only to:

- Fixed variable orderings;
- One-way reading;
- Bounded depth;
- A single proof system;
- Monotone circuits;
- Specific linear programming representations.

Lower bounds in restricted models are still valuable, but their scope of applicability must be clearly marked.

## 2.6 Barrier Compatibility

The candidate proof strategy needs to check whether it:

- Completely relativizes;
- Falls under the natural proofs framework;
- Is still covered by the algebrization barrier;
- Implicitly relies on unproven cryptographic assumptions.

---

# III. The Not-Equals Team Plays: Residual Distinguishability

Let $\varphi(z_1,\ldots,z_n)$ be a Boolean formula. Select a set of processed variables:

$$
S\subseteq\{z_1,\ldots,z_n\}.
$$

For each partial assignment

$$
\alpha\in\{0,1\}^{S},
$$

substitute it into the formula to obtain the residual function:

$$
\varphi\!\upharpoonright_{\alpha}.
$$

Two partial assignments $\alpha,\beta$ are considered equivalent if they yield the same result for all extensions of unassigned variables:

$$
\alpha\sim_S\beta
\iff
\forall\gamma\in\{0,1\}^{\bar S},
\quad
\varphi(\alpha,\gamma)=\varphi(\beta,\gamma).
$$

Define the set of residual classes:

$$
\operatorname{Res}_S(\varphi)
=
\left\{
\varphi\!\upharpoonright_{\alpha}
:
\alpha\in\{0,1\}^{S}
\right\}/\equiv.
$$

Its cardinality is:

$$
N_{\mathrm{res}}(\varphi,S)
=
\left|
\operatorname{Res}_S(\varphi)
\right|.
$$

Then define the residual distinguishable load:

$$
H_{\mathrm{res}}(\varphi,S)
=
\log_2N_{\mathrm{res}}(\varphi,S).
$$

Intuitively, if two partial histories leave different residual functions, they cannot be unconditionally merged by an exact solver; because there exists some future input that requires the two to output different results.

---

# IV. Candidate Lemma: State Lower Bound on Cuts

Consider a class of deterministic state machines that read variables in a fixed order, and after passing through set $S$, only preserve past information via an internal state $q$, never re-reading the variables in $S$ thereafter.

If two partial assignments $\alpha,\beta$ are mapped to the same state:

$$
q(\alpha)=q(\beta),
$$

but:

$$
\alpha\not\sim_S\beta,
$$

then there exists some future extension $\gamma$ such that:

$$
\varphi(\alpha,\gamma)
\neq
\varphi(\beta,\gamma).
$$

Since the machine receives the same future input from the same state, its subsequent behavior will be completely identical, thus at least one input will be misjudged.

Therefore, in this model:

$$
|Q_S|
\geq
N_{\mathrm{res}}(\varphi,S),
$$

or equivalently:

$$
\log_2|Q_S|
\geq
H_{\mathrm{res}}(\varphi,S).
$$

This is a genuine semantic lower bound: it does not rely on the superficial syntax of the residual formulas, but on whether they represent different Boolean functions.

The Not-Equals Team thus proposes their first-version claim:

> If one can find a family of SAT instances such that any reasonable computational decomposition inevitably passes through a cut with a super-polynomial residual distinguishable load, it may force any exact state machine to expend super-polynomial state or time resources.

---

# V. The Equals Team Counterattacks: You Only Caught a Fixed Channel

The Equals Team admits the above lemma is valid within the specified model, but immediately proposes five escapes.

## 5.1 Variable Ordering Escape

A formula under the variable ordering

$$
z_1,z_2,\ldots,z_n
$$

might generate a massive number of residual classes, but could be highly compressed under another ordering.

Therefore, one should consider:

$$
\min_{\pi}
\max_i
H_{\mathrm{res}}(\varphi,S_{\pi,i}),
$$

where $S_{\pi,i}$ is the first $i$ variables of ordering $\pi$.

But even if it is large for all linear orderings, it only restricts ordered decision graphs and similar models.

## 5.2 Revisit Input Escape

A general Turing machine can read the input multiple times and does not have to permanently forget read variables after a single cut. It can trade time for space, recomputing previous information.

Therefore:

$$
\text{Cut state lower bound}
\not\Rightarrow
\text{General time lower bound}.
$$

## 5.3 Global Summary Escape

A large number of residual functions does not mean they cannot share a short algebraic, spectral, or structural representation.

A massive number of distinct objects might be generated by a small number of parameters and a unified evaluation procedure.

## 5.4 Auxiliary Variable Escape

The solver can introduce new intermediate variables, extend dimensions, or rewrite constraints, such that an originally difficult projection has a shorter description in a higher-dimensional space.

Thus, a representation explosion in the original space does not necessarily preclude an extended representation.

## 5.5 Non-Hierarchical Algorithm Escape

Algorithms might not operate in a "read half first, then read the other half" mode. They can interleave processing, propagate locally, backtrack, learn conflicts, rewrite formulas, or directly compute some global invariant.

The Equals Team's conclusion is:

$$
\boxed{
H_{\mathrm{res}}
\text{ is an in-model lower bound component, not a general computational invariant.}
}
$$

---

# VI. First Set of Test Questions: A Large Candidate Space Does Not Equal a Large Residual Load

## 6.1 Parity Function

Let:

$$
\operatorname{PARITY}(x_1,\ldots,x_n)
=
x_1\oplus\cdots\oplus x_n.
$$

There are a total of:

$$
2^n
$$

inputs, but no matter how many bits have been read, one only needs to preserve the current parity:

$$
q\in\{0,1\}.
$$

Therefore:

$$
N_{\mathrm{res}}\leq2.
$$

This shatters a common erroneous line of reasoning:

$$
\text{Exponentially large number of candidates or inputs}
\not\Rightarrow
\text{Exponentially large required state}.
$$

## 6.2 Symmetric Boolean Functions

If the function only depends on the number of $1$s in the input, the machine can preserve the count:

$$
0,1,\ldots,n.
$$

The states only require a polynomial quantity, even if the complete truth table contains $2^n$ inputs.

This illustrates again:

$$
\text{Huge truth table}
\not\Rightarrow
\text{Structurally incompressible}.
$$

## 6.3 Fixed Ordering Difficulty and Representation Rewriting

Certain Boolean functions require very large representations in specific ordered binary decision diagrams, but after changing the variable ordering or converting to a more general knowledge compilation language, they might shrink significantly.

Knowledge compilation theory therefore simultaneously compares:

$$
\text{Representation succinctness}
$$

and:

$$
\text{Queries/transformations computable in polynomial time}.
$$

This supports the Not-Equals Team's intuition that "complexity might transfer," while simultaneously supporting the Equals Team's counterattack that "no single representation is always optimal."

---

# VII. The Not-Equals Team Upgrades: From Single Cuts to Minimax Cuts

The Not-Equals Team attempts to incorporate the freedom of variable ordering as well.

For some allowed decomposition strategy $\Pi$, let:

$$
\operatorname{Load}(\varphi,\Pi)
=
\max_{c\in\operatorname{Cuts}(\Pi)}
H_{\mathrm{res}}(\varphi,c).
$$

Then take the minimum over all polynomially describable decomposition strategies:

$$
\operatorname{MCL}(\varphi)
=
\min_{\Pi\in\mathcal P}
\operatorname{Load}(\varphi,\Pi).
$$

This quantity can be called:

$$
\boxed{\text{Minimax Distinguishable Load}}
$$

The intent is: the algorithm can choose the optimal path itself, but must still bear the worst-case cut somewhere.

If there exists a formula family $\{\varphi_n\}$ such that:

$$
\operatorname{MCL}(\varphi_n)
\geq
n^{\omega(1)},
$$

it seems to preclude polynomial state summarization.

---

# VIII. The Equals Team's Second Counterattack: This Starts to Become a Circular Definition

The Equals Team points out:

If $\mathcal P$ contains all possible polynomial algorithm decompositions, then computing or lower-bounding

$$
\operatorname{MCL}
$$

itself is almost equivalent to proving a lower bound for all algorithms.

If $\mathcal P$ only contains a manageable restricted family, then the resulting conclusion is still just a restricted model lower bound.

Thus a dilemma emerges:

$$
\mathcal P\text{ is too small}
\Rightarrow
\text{Cannot cover all algorithms},
$$

$$
\mathcal P\text{ is too large}
\Rightarrow
\text{Candidate quantity is hard to characterize independently, or even circular}.
$$

This is the first major failure result of this round:

> Directly adding "taking the minimum over all representations" into the definition does not automatically produce a cross-representation theorem; it might merely hide the universal quantifier to be proven inside the name of the invariant.

---

# IX. Qualification Tests for Other Candidate Invariants

## 9.1 Constraint Interaction Width

Candidate idea: SAT difficulty stems from non-localizable high-order interactions between constraints.

Possible metrics include graph width, tree width, hypergraph width, or elimination width.

Pros:

- Can explain efficient algorithms on many restricted structures;
- Directly related to dynamic programming and variable elimination.

Cons:

- General algorithms do not have to follow a given decomposition;
- Formulas can be rewritten via auxiliary variables;
- High graph width does not automatically imply super-polynomial time for all algorithms.

**Verdict:** A powerful parameter, but not yet a general invariant.

## 9.2 Proof Width and Proof Length

For unsatisfiable formulas, one can study the width, space, and length required for a refutation proof. In resolution proof systems, a profound relationship exists between width and proof length; certain formulas have exponentially long resolution proofs because they require large width.

Pros:

- Can transform the judgment of "no solution" into proof resources;
- Mature lower bound methods exist.

Cons:

- Lower bounds depend on the proof system;
- A long proof in one system does not preclude a short proof in another stronger system;
- Covering all polynomial-time algorithms would approach the core hard problems of general propositional proof complexity.

**Verdict:** A strong local weapon, but easily escaped by "switching proof systems."

## 9.3 Extension Complexity

Representing combinatorial problems as polytopes, studying whether there exist extended representations in higher dimensions but with a small number of inequalities.

Important results have already proven that polytopes for the Traveling Salesperson, Cut, and Stable Set problems do not have polynomial-sized specific linear extended formulations.

Pros:

- Allows the introduction of auxiliary dimensions, already transcending direct descriptions in the original space;
- Can prove genuine exponential representation lower bounds.

Cons:

- Still restricted to linear programming/polytope representation models;
- Cannot preclude non-linear, non-convex, combinatorial, or general Turing algorithms.

**Verdict:** Demonstrates an example where "even dimensional extension cannot always rescue," but does not equate to $P\neq NP$.

## 9.4 Information Content

Candidate idea: The witness space contains exponential information, therefore a deterministic machine must process exponential information.

Counterexample: The final decision output is only one bit, and many functions over exponential input spaces have short summaries.

**Verdict:** Unstructured raw information content is insufficient.

## 9.5 Historical Construction Cost

Candidate idea: If a mathematical compressor is extremely difficult to discover, its cognitive generation cost forms a blockade.

This quantity applies to agent cognitive dynamics, but does not belong to the traditional runtime complexity of fixed algorithms. As long as the algorithm finitely exists, its historical discovery cost does not affect the $P$ class.

**Verdict:** Retained for meta-level research, must not masquerade as an object-level lower bound.

---

# X. Candidate Invariant Scoring Table

| Candidate Quantity | Semanticity | Cross-Representation | Can Generate Lower Bounds | General Model Coverage | Current Verdict |
|---|---:|---:|---:|---:|---|
| Number of Candidates/Witnesses | Low | Low | Low | Low | Eliminated |
| Truth Table Size | Medium | Low | Low | Low | Eliminated |
| Number of Residual Classes on Fixed Cuts | High | Low to Medium | High (Restricted Models) | Low | Retained as Component |
| Residual Load of Optimal Ordering | High | Medium | Medium to High | Low to Medium | Retained |
| Constraint Interaction Width | Medium to High | Medium | High (Parameterized Models) | Medium-Low | Retained |
| Resolution Proof Width | High | Low | High (Resolution Systems) | Low | Retained |
| Extension Complexity | High | Medium-High | High (Linear Models) | Low | Retained |
| Historical Discovery Cost | High (Meta-Level) | Medium | N/A for Object-Level | N/A | Diverted & Saved |
| Minimum Time Over All Algorithms | High | High | Circular | High | Unqualified |

---

# XI. Official Attack and Defense Records of Both Sides

## 11.1 The Not-Equals Team's Claims

1. Existential quantifier elimination cannot possibly leave absolutely no distinguishable structure behind;
2. For certain formula families, local residual classes, interaction width, and proof width will all explode;
3. Different lower bound models might be observing different projections of the same deeper barrier;
4. The true invariant might not be a single scalar, but a set of load vectors that cannot be simultaneously compressed.

Candidate vector:

$$
\mathbf I(\varphi)
=
\left(
H_{\mathrm{res}},
W_{\mathrm{interaction}},
W_{\mathrm{proof}},
C_{\mathrm{extension}},
P_{\mathrm{precision}}
\right).
$$

The Not-Equals Team changes strategy: no longer demanding that a certain term be large for all representations, but investigating whether a conservation equation exists:

$$
\prod_j
\left(1+I_j\right)
\geq
2^{\Omega(n)}
$$

or:

$$
\sum_j \log(1+I_j)
\geq
\Omega(n).
$$

This is the vectorized version of "complexity cannot disappear, it can only transfer."

## 11.2 The Equals Team's Claims

1. Adding multiple local lower bounds together does not automatically become a general lower bound;
2. Every candidate quantity might be compressed in different representations;
3. If the vector enumeration is incomplete, unknown representations can use unmeasured dimensions to escape;
4. If the vector contains all possible resources, it degenerates back into a circular restatement of the original problem;
5. What $P=NP$ requires is exactly finding a new structure not yet listed in the resource vector.

The Equals Team thus proposes a counter-proposition:

> The so-called cross-representation invariant might not be a fixed quantity at all, but a temporary boundary constantly broken throughout the history of algorithm design. Proving $P\neq NP$ must explain why the next representation revolution cannot exist.

---

# XII. Barrier Review

## 12.1 Relativization Check

Residual distinguishability and communication cut-style arguments often treat sub-computations as black-box interactions. If the proof still holds as-is after adding an arbitrary oracle, one must be wary of the relativization barrier.

**Status:** Not yet passed.

## 12.2 Natural Proofs Check

If the candidate invariant:

- Holds for a large number of functions;
- Is efficiently recognizable;
- Can preclude small circuits;

then it might fall into the typical structure of the natural proofs barrier.

**Status:** High risk, requires subsequent specialized review.

## 12.3 Algebrization Check

If the residual matrix is subsequently characterized using rank, spectral, or polynomial methods, it still needs to be checked whether it is merely an extension of algebrization methods.

**Status:** Not yet initiated.

## 12.4 Restricted Model Misextrapolation Check

Currently, all concrete lemmas only hold for specific cut or state summarization models.

**Status:** Clearly marked, not masquerading as a general proof.

---

# XIII. Erroneous Routes Eliminated in This Round

The following arguments may no longer serve as independent proofs for $P\neq NP$:

1. There are $2^n$ witnesses, so one must check $2^n$ times;
2. The truth table has $2^n$ rows, so any algorithm requires exponential resources;
3. A decision graph with a fixed variable ordering is very large, so no polynomial algorithm exists;
4. A certain proof system requires long proofs, so all solvers are very slow;
5. Defining a quantity by taking the minimum over all algorithms, and then declaring it to be large;
6. Factoring the historical discovery cost of an algorithm into the traditional $P$ class runtime;
7. Multiplying multiple resource metrics that are not yet proven to be complete, and calling it a conservation law.

---

# XIV. Tentative Results of This Round

## 14.1 Result 1: Found the First Workable Local Invariant

Residual distinguishability indeed forms a semantic state lower bound in the fixed-cut state machine model:

$$
|Q_S|
\geq
N_{\mathrm{res}}(\varphi,S).
$$

This is not a mere syntactic size, but is determined by whether future extensions can distinguish the history.

## 14.2 Result 2: Proved It Is Not Yet Sufficient to Cross All Representations

General algorithms can escape via rearrangement, revisiting, dimensional extension, algebraic summarization, and switching proof systems. Therefore:

$$
H_{\mathrm{res}}
$$

can currently only serve as a component for a cross-representation invariant.

## 14.3 Result 3: The Single Scalar Route Might Be Overly Optimistic

The true candidate might be a resource vector or a simultaneous incompressibility relationship:

$$
\mathbf I
=
(I_1,\ldots,I_k).
$$

But one must avoid missing terms and circular definitions.

## 14.4 Result 4: The Next Core Problem Emerges

To make local distinguishability a general lower bound, one needs to establish:

$$
\boxed{
\text{The computational history of any exact algorithm inevitably induces some analyzable cut.}
}
$$

In other words, instead of fixing the variable ordering, one extracts cuts from the algorithm's own execution trajectory.

---

# XV. Gateway to Round 03

Tentative Topic for Round 03:

## Algorithmic Trajectory Cuts: Must Any Exact Solver Expose a Distinguishable Bottleneck?

Core Question:

Given the computational history of any deterministic algorithm $A$:

$$
q_0\rightarrow q_1\rightarrow\cdots\rightarrow q_T,
$$

can one define a distinguishable relationship between "past information" and "future requirements" from some time cut $t$, and prove that:

$$
\operatorname{StateInfo}(q_t)
+
\operatorname{RemainingWork}(q_t)
$$

at least one term must be super-polynomial?

The Equals Team will claim: algorithms can make information flow, recompute, and re-encode over time; no fixed bottleneck exists.

The Not-Equals Team will claim: no matter how it flows, the causal dependence of the exact answer must pass through certain finite state cuts, thus potentially generating a three-way trade-off among time, space, and distinguishability.

---

# XVI. Historical Dependencies

Dependencies for this round:

1. `00_Mathematical_Construct_State_Machine_Middleware_v1.0.md`
   - Provides formalization, mathematical constructs, base implementations, and state transition chains.
2. `01_Round_01_Existential_Quantifier_State_Collapse.md`
   - Provides the existential quantifier compressor $\mathcal C_{\exists}$, the common resource ledger, and the dual-hypothesis arena.
3. Neo.K's existing P/NP dynamic rate series
   - Provides the cognitive dynamics background of search, generation, computation, verification, knowledge condensation, and complexity transfer.

---

# XVII. External Theoretical References

1. A. Darwiche and P. Marquis, “A Knowledge Compilation Map,” *Journal of Artificial Intelligence Research*, 2002.
   - Used to distinguish between representation succinctness and efficiently supported queries/transformations.
2. R. E. Bryant, “Graph-Based Algorithms for Boolean Function Manipulation,” *IEEE Transactions on Computers*, 1986.
   - Used for ordered binary decision diagrams and variable-ordering-dependent representations.
3. E. Ben-Sasson and A. Wigderson, “Short Proofs Are Narrow—Resolution Made Simple,” *Journal of the ACM*, 2001.
   - Used for the relationship between resolution proof width and length.
4. S. Fiorini, S. Massar, S. Pokutta, H. R. Tiwary, and R. de Wolf, “Exponential Lower Bounds for Polytopes in Combinatorial Optimization,” *Journal of the ACM*, 2015.
   - Used for extension complexity and linear representation lower bounds.
5. Myhill–Nerode type distinguishability principle.
   - The conceptual source of the residual distinguishability lower bound in this round; this document only uses it as an analogy and starting point for extension to finite state cuts, without claiming to have established a general Turing machine version.

---

## Verdict for This Round

$$
\boxed{
\text{The Not-Equals Team has acquired a local weapon, but not yet a cross-representation artifact.}
}
$$

$$
\boxed{
\text{The Equals Team has successfully escaped, but has not yet demonstrated a true polynomial existential quantifier compressor.}
}
$$

Therefore, the tentative score is:

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

The score is merely a game interface, not mathematical evidence.