# Dimensional Chess C7: Horizon-Safe State Projection

**Date:** 15 September 2026  
**Status:** independently verified finite computation  
**Claim boundary:** exact bounded-mate result; not an unbounded WDL solution of chess

## Result

From the orthodox initial position, neither White nor Black can force checkmate
within nine plies:

\[
B_W(s_0,9)=0,\qquad B_B(s_0,9)=0.
\]

This extends the independently verified frontier from seven to nine plies. It
does not determine whether chess is a win, draw, or loss under unlimited optimal
play. The initial WDL interval therefore remains

\[
I(s_0)=[-1,+1].
\]

## Exact predicate

For designated attacker \(P\), the bounded predicate is

\[
B_P(s,d)=
\begin{cases}
1,&s\text{ is checkmate won by }P,\\
0,&s\text{ is a terminal draw or }d=0,\\
\bigvee_{a\in\mathcal L(s)}B_P(T(s,a),d-1),&\operatorname{turn}(s)=P,\\
\bigwedge_{a\in\mathcal L(s)}B_P(T(s,a),d-1),&\operatorname{turn}(s)\ne P.
\end{cases}
\]

The defender's ability to claim a draw is modeled both at the current node and
after an intended move. The attacker may ignore an optional draw because the
predicate asks whether that attacker can force checkmate. Checkmate is tested
before draw claims, as required by orthodox terminal precedence.

## Projection theorem

Let \(h=(p_0,p_1,\ldots,p_t)\) be the sequence of repetition keys on a search
path and let the total root horizon be \(D\). A repeated full chess position has
the same player to move, so recurrence intervals are even. A two-ply recurrence
is impossible: after the first player moves, the opponent cannot restore the
first player's piece and also restore their own move in one ply without changing
piece placement, material, castling rights, or en-passant state. Hence identical
positions are separated by at least four plies.

A position first encountered at ply \(i\) therefore cannot have its third
occurrence before ply \(i+8\). For a threefold-claim horizon \(D\), only positions
with

\[
i\le D-8
\]

can affect the result. C7 memoizes the current repetition key, remaining depth,
attacker, and multiplicities only for this prefix of repetition candidates. It
drops the fullmove number always. It drops the halfmove clock exactly when the
fifty-move threshold is globally unreachable inside the horizon.

At \(D=9\), only the initial position and the position after the first move can
possibly become threefold. All later path history is a provably irrelevant
coordinate for this finite theorem. Identifying states that differ only in those
coordinates is the C7 dimensional lift.

## Ordering experiments

The first C7 experiment separated attacker and defender ordering. On the
five-ply White-attacker negative proof, the defender ordering fixed the proof
node count while attacker ordering did not:

| Defender order | Proof calls | Generated edges | Measured time |
|---|---:|---:|---:|
| Lexical | 7,480 | 15,988 | 1.665 s |
| C6 dependency | 7,536 | 16,458 | 6.627 s |
| Checks/captures | 9,992 | 18,627 | 7.386 s |

This is consistent with proof polarity: a negative attacker claim must reject
all attacking moves, whereas one defender escape refutes each candidate line.
The result is task-specific evidence, not a universal theorem about lexical
order.

Two alternatives were rejected:

- A richer escape heuristic used 9,926 calls and 21,490 edges at five plies and
  took 95.13 seconds. Feature cost dominated any ordering benefit.
- A naive best-first proof-number search expanded 40,316 nodes and generated
  743,471 children in 32.44 seconds at five plies. It was much worse than the
  depth-first lexical baseline for this negative certificate.

## Seven-ply quotient baseline

Below eight plies, no threefold claim is reachable from the initial history and
the halfmove threshold is also unreachable. C7 removes all history and clock
coordinates except the repetition key itself.

| Attacker | C7 calls | Generated edges | Time |
|---|---:|---:|---:|
| White | 95,718 | 172,970 | 15.737 s |
| Black | 10,551 | 69,667 | 2.152 s |

The earlier independently written lexical verifier used 106,322 and 15,082
calls, respectively. Combined calls fall from 121,404 to 106,269, a 12.47%
reduction, without changing either Boolean result.

## Nine-ply certificate

| Attacker | Result | Proof calls | Generated edges | Cache hits | Horizon nodes | Time |
|---|---|---:|---:|---:|---:|---:|
| White | no forced mate | 2,951,587 | 5,259,337 | 1,437,821 | 1,308,014 | 575.877 s |
| Black | no forced mate | 127,991 | 736,248 | 59,263 | 30,841 | 23.080 s |

The White frontier grew by a factor of 30.84 from seven to nine plies; Black's
grew by a factor of 12.13. The quotient makes the computation feasible but does
not remove exponential growth.

An intentionally over-conservative pilot retained the multiplicity of every
visited position. It was stopped after about 21 minutes because it had grown to
roughly 3.5 GB without completing. The horizon-safe candidate projection
completed the White proof in 575.9 seconds and used hundreds of megabytes rather
than multiple gigabytes. The stopped pilot is an engineering observation, not
part of the Boolean certificate.

## Independent verification

The verifier imports no C7 solver code. It independently reconstructs the
candidate prefix, defender draw actions, and AND/OR recurrence using the audited
legal-state engine. It reproduces every reported result and all node, edge,
cache, horizon, and terminal counts at depths seven and nine.

It also exhaustively checks 400 legal two-ply paths from the initial position
and 8,902 legal two-ply paths from all first-ply states, finding no two-ply
return. Explicit legal knight cycles confirm that the initial position first
reaches three occurrences at ply eight and a position first seen after move one
first reaches three occurrences at ply nine. Audit status: **PASS**.

## What is and is not solved

C7 proves a new finite statement and supplies a reusable state-quotient theorem:
terminal-rule coordinates need be retained only when they can cross their
threshold within the remaining horizon. It does not supply a strategy for
unbounded optimal play and does not narrow the root WDL interval.

The next wall is no longer move ordering. A full solution needs proof-carrying
lower and upper bounds that summarize large sets of continuations, together
with a complete treatment of every terminal rule. Without a sound abstraction
whose intervals separate at the root, extending the horizon remains exponential.