// =============================================================================
// Strategy as Theorem: Deriving Optimal Feedback Laws from
// Bellman-Invariant Bases via Operator Iteration
// =============================================================================
//
// An arXiv paper presenting a mechanizable pipeline for discovering
// Bellman-invariant bases via Bellman pre-image iteration, yielding
// closed-form optimal feedback laws without state-space enumeration.
// Tic-Tac-Toe serves as the complete worked example.
//
// The executable appendix is the examples/games/ directory:
//   tictactoe_rules.kleis      — Game specification (27 axioms)
//   tictactoe_topology.kleis   — Mask derivation from grid geometry
//   ttt_krylov.kleis           — Bellman pre-image iteration (measure discovery)
//   ttt_synthesis.kleis        — Z3 synthesis of priority ordering
//   tictactoe_bellman.kleis    — Bellman derivation of feedback law
//   tictactoe_complete_proof.kleis — Complete safety proof (96 nodes)
//   ttt_match/prove_t2_empty.py — T⁻² termination proof
//   ttt_match/ttt_match.py     — Match runner vs perfect minimax
//
// Compile:
//   kleis test --raw-output --example compile \
//       docs/papers/strategy_synthesis_paper.kleis > strategy_synthesis_paper.typ
//   typst compile strategy_synthesis_paper.typ strategy_synthesis_paper.pdf
//
// =============================================================================

import "stdlib/prelude.kleis"
import "stdlib/templates/arxiv_paper.kleis"

// =============================================================================
// Metadata
// =============================================================================

define paper_title = "Strategy as Theorem: Deriving Optimal Feedback Laws from Bellman-Invariant Bases via Operator Iteration"

define paper_authors = [
    Author("Engin Atik", "1")
]

define paper_affiliations = [
    Affiliation(1, "Kleis Research", "https://kleis.io")
]

define paper_abstract = "We present a mechanizable pipeline that derives optimal game strategy from rules alone — no training, no human strategic input, and no search over the game tree. The pipeline discovers a minimal Bellman-invariant basis: a set of measures over which the dynamic programming recursion closes and the optimal policy becomes a closed-form algebraic function. The measures are not designed by a strategist but generated as successive Bellman pre-images of the terminal predicate, forming a discrete Krylov sequence that terminates at bounded depth. Given only a game's syntactic rules, the methodology: (1) seeds the iteration with the terminal value predicate; (2) computes Bellman pre-images — each level yielding a new measure whose satisfaction guarantees the previous level regardless of opponent response; (3) terminates when no deeper pre-image produces an actionable advantage; and (4) synthesizes the priority ordering and thresholds via SMT solver, producing the feedback law as the unique satisfying assignment. The resulting controller is a memoryless combinational circuit — the Bellman recursion has been compiled away. Using Tic-Tac-Toe as a complete worked example, we derive from the game definition: five measure families as two Krylov levels applied to both players plus one residual; a termination proof (exhaustive computation confirms every deeper candidate admits a spoiling response); and Z3 synthesis of both the unique priority ordering and a missing measure from an incomplete basis. Correctness is confirmed by exhaustive play against a perfect minimax opponent: 0 losses across all 549 reachable opponent-move sequences. The central claim: what appears to be strategic intelligence is the fixed point of an operator iteration over predicate space. The search tree was never the fundamental object; it was one method for computing a controller that has a closed form once the right coordinates are found."

define paper_keywords = "Bellman-invariant basis, operator iteration, representation discovery, feedback control law, formal verification, game theory, SMT solvers, strategy synthesis, Skolem functions, knowledge creation, Hamilton-Jacobi-Bellman, Z3"

// =============================================================================
// Section 1: Introduction
// =============================================================================

define sec_intro = ArxivSection("Introduction",
"The dominant paradigm in game-playing AI treats strategy as an emergent property of massive computation: deep reinforcement learning systems like AlphaZero [1] discover strategies by playing millions of games against themselves, distilling statistical patterns into neural network weights. This approach produces superhuman play but offers no formal guarantee of correctness, no explanation of _why_ a strategy works, and no transferable structural insight.

We present an alternative: a mechanizable pipeline that _derives_ optimal play from a game's syntactic rules alone, without training data, without human strategic input, and without searching the game tree. The pipeline produces not merely a strategy but the _representation_ that makes the strategy algebraically inevitable.

The thesis rests on a structural observation: in any finite game with rules, the space of _predicates_ (structural properties of board states) is vastly smaller than the space of _positions_ (concrete board configurations). Strategic intelligence operates in predicate space. The pipeline works there too.

Two concepts from control theory organize the derivation. The _Bellman equation_ expresses optimality recursively: the value of a state equals the best immediate reward plus the value of the successor state under optimal play. A _Bellman pre-image_ of a predicate $phi$ is the set of states from which some action guarantees $phi$ will hold at the next step, regardless of the opponent's response — it answers the question 'what must be true _now_ so that $phi$ is achievable _next_?' Iterating this operator produces a sequence of increasingly deep strategic requirements: level 0 is 'can win immediately,' level 1 is 'can guarantee reaching a winning position,' and so on. Each level introduces a genuinely new measure — a structural property of the board that was not expressible at the previous level. The iteration terminates when the next pre-image adds nothing new: either it is empty (no position guarantees the deeper property) or it is already captured by existing measures. We call this a _Krylov iteration_ by analogy with the numerical method where repeated application of an operator to a seed vector generates an expanding basis until saturation.

The methodology proceeds by operator iteration:

+ _The terminal predicate seeds the sequence._ Every game defines a terminal condition (winning). This is level zero.
+ _Bellman pre-images generate successive measures._ At each level, the question is: what board property _guarantees_ achieving the previous level's predicate regardless of opponent response? The answer is the next measure. Each step takes the Bellman pre-image of the previous level's predicate — the same operation defined above, applied iteratively.
+ _Termination occurs when no deeper guarantee exists._ The iteration terminates at bounded depth: beyond some level, every candidate position admits a spoiling response by the opponent — a counter-move that negates the deterministic advantage. For each game, this is established by checking all candidate positions at the next depth level.
+ _SMT synthesis closes the loop._ Given the complete measure basis, Z3 synthesizes the unique priority ordering and activation thresholds from critical-position constraints. The feedback law is the satisfying assignment of the resulting constraint system.

The result is a _compiled controller_: a memoryless algebraic function from board state to optimal move, requiring no runtime search, no stored game tree, no recursion. The dynamic programming that in principle requires exhaustive tree traversal has been algebraically collapsed into a circuit.

A clarification on 'search': the pipeline does _not_ avoid computation. It avoids computation over the _game tree_. Z3 searches constraint space; the termination proof enumerates states. But these operate in predicate space (bounded by iteration depth, typically 2-3 levels) rather than game-tree space (exponential in game length). For Tic-Tac-Toe: predicate space has 5 dimensions; the game tree has 255,168 terminal nodes. The compression ratio is the content of the representation theorem.

The philosophical claim is precise: the intelligence-like step is _representation discovery_ — finding coordinates over which optimal behavior becomes closed-form. Once the representation is found, the passage from rules to strategy is deduction. The search tree was never the fundamental object; it was one method for computing a controller that admits a symbolic solution in the right coordinate system.

We demonstrate the complete pipeline on Tic-Tac-Toe, chosen not for difficulty but for completeness: it is the simplest game where the full derivation chain — from terminal predicate through Krylov iteration through Bellman compression to verified unbeatable play — can be exhibited in a single paper with every step machine-checked.

The contributions are:
+ A _definition_ of Bellman-invariant basis (closure + sufficiency) as the formal criterion for a complete strategic representation.
+ A _discovery procedure_ via Krylov iteration: successive Bellman pre-images of the terminal predicate, with Z3 synthesis of missing measures from incomplete bases.
+ A _termination proof_: exhaustive computation confirms that the pre-image chain terminates at depth 1 for Tic-Tac-Toe — every depth-2 candidate admits a spoiling response.
+ A _synthesis result_: Z3 finds the unique priority ordering and thresholds from critical-position constraints, producing the feedback law as the sole satisfying assignment.
+ A _verification_ of correctness by exhaustive play against a perfect minimax opponent: 0 losses across all 549 reachable opponent-move sequences.
+ A _mechanized_ implementation in the Kleis formal verification language [2] with Z3 as the backend solver.

Tic-Tac-Toe serves as the proof-of-concept. The methodology applies to any finite game where the Bellman pre-image chain terminates at bounded depth.")

// =============================================================================
// Section 2: Related Work
// =============================================================================

define sec_related = ArxivSection("Related Work",
"Game-playing AI has followed two trajectories: search-based methods (minimax [8], alpha-beta, Monte Carlo tree search) that explore game trees explicitly, and learning-based methods (temporal difference learning, deep reinforcement learning) that approximate value functions from self-play data.

AlphaZero [1] unified these by using a neural network to guide Monte Carlo tree search, achieving superhuman performance in chess, shogi, and Go from self-play alone. The resulting strategies were long considered opaque — network weights encode no human-readable principles, and correctness is statistical rather than formal. Recent work by Schut et al. [11] partially addresses this: they extract concept vectors from AlphaZero's internal representations via convex optimization, filter for novelty, and successfully transfer discovered chess concepts to grandmasters. This demonstrates that structural knowledge _exists_ inside trained networks but must be excavated post-hoc. Our approach inverts this: we derive the structural knowledge _a priori_ from the rules, before any training occurs.

Reactive synthesis [12] is the closest methodological relative. In this framework, a specification is reduced to a two-player game on a graph, and winning strategies are computed via fixpoint iteration of a predecessor operator: given a target set $T$, the attractor $\"Attr\"(T) = T union \"Pre\"(T) union \"Pre\"^2(T) union dots$ accumulates all states from which the system can force reaching $T$. This is structurally identical to our Bellman pre-image iteration. The critical difference is the _space_ of iteration: reactive synthesis iterates over the concrete game graph (whose size is the state space), while our method iterates over predicate space (whose size is bounded by the operator depth — typically 2-3 levels regardless of state-space size). Bansal et al. [13] recently demonstrated efficient symbolic fixpoint algorithms for LTL game solving using SMT solvers, showing that formal backends can scale beyond BDD-based representations.

Formal methods have been applied to combinatorial games primarily for _verification_ rather than _synthesis_. Heule et al. [3] used SAT solvers to resolve the boolean Pythagorean Triples problem; Konev and Lisitsa [4] settled the Erdős discrepancy conjecture via SAT. These demonstrate that solvers can establish game-theoretic facts, but they operate by exhaustive case analysis over concrete configurations — essentially mechanized brute force in state space.

Program synthesis from specifications [5] is closer in spirit: given a logical specification $phi(x, f(x))$, synthesize a function $f$ satisfying it. Counterexample-guided inductive synthesis (CEGIS) [6] iterates between candidate generation and counterexample production. Our work differs in that we do not synthesize a _function_ (a move table mapping positions to actions) but derive _structural principles_ (a measure basis and priority ordering) from which the move function follows as a theorem.

The distinction between solutions and strategies is central. A solution is a complete move table requiring enumeration proportional to the game tree. A strategy is a structural principle: a finite set of predicates and a priority ordering over them, from which the correct move at any position is computable in constant time. Reactive synthesis finds a strategy _over the game graph_; we find one _over predicate space_. The contribution is showing that, for games where the Bellman pre-image chain terminates at bounded depth, the latter is both sufficient and vastly more compact.")

// =============================================================================
// Section 3: Game Specification
// =============================================================================

define sec_specification = ArxivSection("The Game Specification",
"We encode Tic-Tac-Toe as a first-order theory over integers. The encoding choices are minimal and canonical: 9 cells map to bit positions 0-8, and set membership is represented as bit extraction via $\"mod\"$/$\"div\"$.")

define subsec_board = ArxivSubsection("Board Representation",
"A game state is a triple $(b_x, b_o, t)$ where $b_x, b_o in {0, dots, 511}$ are 9-bit integers encoding X's and O's occupied cells, and $t in {1, 2}$ indicates whose turn it is. Cell $i$ is occupied by X iff $\"bit\"(b_x, i) = 1$, where:
$ \"bit\"(x, i) = \"mod\"(\"div\"(x, 2^i), 2) $
This definition is unrolled for $i in {0, dots, 8}$, giving Z3 a concrete ground-truth reduction for each bit position. No uninterpreted functions, no quantifier triggers — pure integer arithmetic.")

define subsec_bitops = ArxivSubsection("Bitwise Operations as Arithmetic",
"Bitwise AND and OR are defined as direct arithmetic formulas over all 9 bits:
$ \"bit_and\"(x, y) = sum_(i=0)^8 \"bit\"(x, i) dot \"bit\"(y, i) dot 2^i $
$ \"bit_or\"(x, y) = sum_(i=0)^8 (\"bit\"(x, i) + \"bit\"(y, i) - \"bit\"(x, i) dot \"bit\"(y, i)) dot 2^i $

This encoding is critical for avoiding E-matching explosions. A natural alternative — defining $\"bit_and\"$ via per-bit universally-quantified axioms like $forall i. \"bit\"(\"bit_and\"(x,y), i) = \"bit\"(x,i) dot \"bit\"(y,i)$ — triggers unbounded quantifier instantiation when Z3 encounters concrete board values, leading to contradictions or timeouts. The direct arithmetic formula keeps all reasoning in the quantifier-free fragment: when boards are concrete integers, every $\"bit\"$ call reduces to 0 or 1 by ground arithmetic, and Z3 solves the resulting constraints without search.")

define subsec_winmasks = ArxivSubsection("The Win Matrix",
"The 8 winning configurations are encoded as integer masks:

$ bold(W) = {7, 56, 448, 73, 146, 292, 273, 84} $

These correspond to the 3 rows, 3 columns, and 2 diagonals of the $3 times 3$ grid. A player with board $b$ has won iff $exists k in {0, dots, 7}: \"bit_and\"(b, W_k) = W_k$.

The complete specification comprises 27 axioms: 9 bit-extraction definitions, 1 AND formula, 1 OR formula, 1 set-bit formula, 1 popcount formula, 8 mask constants, 2 win-detection axioms, 1 legality axiom, 2 move-application axioms, 1 alternation invariant, and 1 termination condition.")

// =============================================================================
// Section 4: Strategy Derivation
// =============================================================================

define sec_derivation = ArxivSection("Strategy Derivation from Mask Geometry",
"We now pose structural questions to Z3 about the 8 mask constants and prove that the answers establish the geometric foundations of the strategy. Each theorem is verified in under 2 seconds as a ground arithmetic assertion — no game-tree search, no quantifier instantiation over positions. The complete feedback law, which combines these properties into an actionable controller, is derived in Section 7 via Bellman synthesis.")

define subsec_density = ArxivSubsection("Theorem 1: Center Gravity",
"Define the _density_ of cell $i$ as the number of winning masks containing it:
$ \"density\"(i) = sum_(k=0)^7 \"bit\"(W_k, i) $

Z3 computes from the 8 mask constants:
$ \"density\"(4) = 4 $
$ \"density\"(0) = \"density\"(2) = \"density\"(6) = \"density\"(8) = 3 $
$ \"density\"(1) = \"density\"(3) = \"density\"(5) = \"density\"(7) = 2 $

*Theorem (Center Gravity):* Cell 4 (the center) has strictly maximum density among all cells. The strict ordering Center $>$ Corner $>$ Edge is a theorem of the mask constants.

This theorem requires no game-tree reasoning. It is a static geometric fact about which cells participate in the most winning configurations. Z3 proves it by evaluating $\"mod\"$/$\"div\"$ chains on concrete integers — pure arithmetic.")

define subsec_independence = ArxivSubsection("Theorem 2: Center Line Independence",
"The 4 winning lines passing through the center (row 1, column 1, main diagonal, anti-diagonal) use the following non-center cells:

- Row 1 ($W_1 = 56$): cells 3, 5
- Column 1 ($W_4 = 146$): cells 1, 7
- Main diagonal ($W_6 = 273$): cells 0, 8
- Anti-diagonal ($W_7 = 84$): cells 2, 6

*Theorem (Line Independence):* These 4 pairs partition all 8 non-center cells. Each non-center cell appears in exactly one center-line. Formally: for each $j in {0,1,2,3,5,6,7,8}$, exactly one of the four center-masks has $\"bit\"(W_k, j) = 1$.

*Consequence:* No single opponent move can block more than one center-line. Blocking all 4 requires at least 4 separate moves — which is all the moves the second player gets in a 9-cell game. This means the opponent must dedicate _every_ move to defensive blocking, leaving no resources for their own offense. If they play even one non-blocking move, the center player can complete an undefended line.

This theorem establishes why density alone implies strategic pressure: the center's 4 lines are not merely numerous but _structurally independent_, making simultaneous defense all-consuming.")

define subsec_fork = ArxivSubsection("Theorem 3: Fork Unblockability",
"A _threat_ on mask $W_k$ exists when a player occupies 2 of the 3 cells in $W_k$ and the third is empty. A _fork_ is two simultaneous threats with distinct empty target cells.

*Theorem (Fork Unblockability):* If player X has threats on masks $W_j$ and $W_k$ with empty targets $t_j != t_k$, then no single move by O can neutralize both threats.

_Proof (verified by Z3):_ A single move sets exactly one bit. With $t_j != t_k$, occupying $t_j$ leaves $t_k$ open (and vice versa). Z3 verifies this on a concrete fork position: $b_x = 81$ (cells 0, 4, 6), $b_o = 6$ (cells 1, 2), threats on $W_6$ (target: cell 8) and $W_3$ (target: cell 3). Setting bit 8 in $b_o$ does not set bit 3, and setting bit 3 does not set bit 8.

The theorem follows from _alternation_ (one move per turn) interacting with _geometry_ (distinct targets). It requires no game-tree lookahead — the unblockability is structural.")

define subsec_prevention = ArxivSubsection("Theorem 4: Center Prevents Immediate Fork",
"*Theorem:* After X occupies the center and O responds with any single cell, O has zero threats (and therefore zero fork potential).

_Proof:_ A threat requires $\"popcount\"(\"bit_and\"(b_o, W_k)) = 2$ for some $k$. After one O move, $\"popcount\"(b_o) = 1$. Since $\"bit_and\"(b_o, W_k)$ can have at most $min(\"popcount\"(b_o), \"popcount\"(W_k))$ bits set, and $\"popcount\"(b_o) = 1 < 2$, no threat can exist. Z3 verifies this for all 8 masks against both symmetry classes of O's response (corner and edge).")

define subsec_hierarchy = ArxivSubsection("Theorem 5: The Density Hierarchy",
"*Theorem:* The strict ordering $\"density\"(\"Center\") > \"density\"(\"Corner\") > \"density\"(\"Edge\")$ holds, with values $4 > 3 > 2$.

Combined with Line Independence (Theorem 2), this establishes density as a _residual tiebreaker_: when higher-priority concerns (winning, blocking, forking) do not distinguish between candidate moves, density selects the move participating in the most winning configurations. The full priority ordering — win, block, fork, prevent opponent fork, then density — is derived in Section 7. Here we establish only that the density ordering exists, is strict, and is a theorem of the mask constants rather than an assumed heuristic.")

// =============================================================================
// Section 5: Complete Safety Verification
// =============================================================================

define sec_verification = ArxivSection("Complete Safety Verification",
"The geometric theorems of Section 4 establish structural properties of individual measures. The complete feedback law — derived via Bellman synthesis in Section 7 — combines them into a priority ordering: win if possible, block opponent wins, create forks, prevent opponent forks, then maximize density. We now verify that this compiled controller produces unbeatable play against all possible opponent moves.")

define subsec_tree = ArxivSubsection("Verification via Symmetry Reduction",
"Before verifying the feedback law exhaustively, we establish a bound on the verification cost. The key observation: Tic-Tac-Toe has far fewer _strategically distinct_ positions than games. The dihedral group $D_4$ of the square (8 symmetries: 4 rotations, 4 reflections) identifies positions that differ only by a rotation or reflection of the board — the same game viewed from a different seat at the table. Any strategy that works for one position in a $D_4$ orbit works for all members of that orbit.

This collapses the verification task:
+ *X plays by the derived feedback law:* X's choices are fixed (no branching). Only O's responses generate the tree.
+ *$D_4$ equivalence classes:* Two O-responses that differ only by a board symmetry are strategically identical. We need only verify one representative per orbit.

The result: 96 distinct positions (Table 1), down from the raw $9! = 362,880$ complete games. This is a topological bound — the number of strategically distinct situations is determined by the grid's symmetry group, not by any search process. It demonstrates that the space of strategies is vastly smaller than the space of games: a feedback law verified on 96 representatives covers all 362,880 game sequences.

Each of the 96 positions is then verified by Z3 as a ground arithmetic assertion (Section 5.2). The 549 unreduced opponent-move sequences serve as an independent cross-check.")

define table_tree = ArxivTable("tab:tree",
    "Symmetry-reduced game tree structure. X plays by invariant-derived priority; O plays all legal responses modulo $D_4$ equivalence. The 96 positions are determined by topology.",
    "table(
  columns: (auto, auto, auto, auto, auto),
  inset: 8pt,
  align: (center, center, center, center, center),
  table.header([*Ply*], [*Positions*], [*X moves*], [*O moves*], [*Terminal*]),
  [0], [1], [0], [0], [0],
  [1], [1], [1], [0], [0],
  [2], [2], [0], [2], [0],
  [3], [2], [2], [0], [0],
  [4], [12], [0], [12], [0],
  [5], [9], [9], [0], [2],
  [6], [34], [0], [34], [0],
  [7], [24], [24], [0], [21],
  [8], [6], [0], [6], [0],
  [9], [5], [5], [0], [4],
  [*Total*], [*96*], [*41*], [*54*], [*27*],
)"
)

define subsec_invariant = ArxivSubsection("Safety Invariant",
"At each of the 96 positions, we verify the safety invariant:
$ forall k in {0, dots, 7}: quad \"bit_and\"(b_o, W_k) != W_k $

This asserts that O has not completed any winning line. The verification is _ground arithmetic_: for each concrete $b_o$ value at each node, Z3 checks 8 inequality assertions. No universal quantifiers over positions are needed — each node is an independent arithmetic check.

Z3 verifies all $96 times 8 = 768$ assertions in 108 seconds. Every assertion passes.

As an independent cross-check, we also verify the strategy exhaustively _without_ symmetry reduction: a minimax oracle generates all reachable opponent responses, yielding 549 distinct opponent-move sequences. The feedback law is evaluated on each. Result: 0 losses across all 549 sequences — confirming that the symmetry reduction lost no generality.")

// =============================================================================
// Section 6: The Derivation Chain
// =============================================================================

define sec_chain = ArxivSection("The Complete Derivation Chain",
"The full path from game definition to verified optimal play involves no human strategic input at any stage. Each step is either a Z3-verified deduction or an exhaustive computation. We now walk through the reasoning that produces each step from the previous — this is the mechanical derivation that replaces intuition:")

define table_chain = ArxivTable("tab:chain",
    "The derivation chain from game rules to verified feedback law. Each step is mechanized.",
    "table(
  columns: (auto, auto, auto),
  inset: 8pt,
  align: (left, left, left),
  table.header([*Step*], [*Input*], [*Output*]),
  [1. Encoding], [Grid + collinearity + alternation], [8 winning masks],
  [2. Terminal predicate], [Line completion condition], [win_contrib(i) $gt.eq 1$],
  [3. Bellman pre-image], [$T^(-1)$(\"can win immediately\")], [fork_contrib(i) $gt.eq 2$],
  [4. Player swap], [Steps 2--3 applied to opponent], [block_contrib, opp_fork_contrib],
  [5. Termination], [$T^(-2)$ candidates exhaustively checked], [Empty: no deeper measure exists],
  [6. Residual], [Mask geometry (no dynamic content)], [density(i): topological tiebreaker],
  [7. Priority synthesis], [Critical positions $arrow$ Z3 constraints], [Unique ordering with thresholds],
  [8. Verification], [Compiled feedback law vs. all opponent moves], [0 losses across 549 sequences],
)"
)

define subsec_derivation_logic = ArxivSubsection("The Reasoning at Each Step",
"*Step 1 (Encoding).* The game's rules specify that three collinear cells constitute a win on a $3 times 3$ grid. Enumerating all maximal collinear sets yields exactly 8 configurations (3 rows, 3 columns, 2 diagonals), represented as bitmasks. This is combinatorial enumeration, not strategic reasoning — it simply asks 'what are the winning sets?'

*Step 2 (Terminal predicate).* The question: 'can I win on my next move?' Formally: does there exist a cell $i$ such that placing my piece completes a winning line? This defines a measure: $\"win_contrib\"(i) gt.eq 1$ means cell $i$ completes at least one line. This is the terminal value function — the boundary condition for the Bellman recursion.

*Step 3 (Bellman pre-image).* The critical reasoning step. We ask: 'what must be true NOW so that I can guarantee winning on my NEXT move, regardless of what the opponent does in between?' Unpacking this: after I move, the opponent moves, and then I need $\"win_contrib\"(j) gt.eq 1$ for some $j$. For this to be guaranteed _regardless_ of the opponent's intervening move, I need TWO simultaneous threats — because the opponent can block at most one per turn. Thus $T^(-1)(\"win_contrib\" gt.eq 1) = \"fork_contrib\"(i) gt.eq 2$. The pre-image of 'can win immediately' is 'can create an unblockable fork.' This is not a heuristic — it is the unique predicate satisfying the Bellman guarantee condition.

*Step 4 (Player swap).* The game is symmetric between players: what constitutes a winning threat for me is a losing threat from my opponent. Therefore: $\"block_contrib\"(i) = \"win_contrib\"(i, \"their\", \"my\")$ — the opponent's winning move is my blocking move. Similarly: $\"opp_fork_contrib\"(i) = \"fork_contrib\"(i, \"their\", \"my\")$ — the opponent's fork opportunity is my prevention priority. This is not a new iteration of the Bellman operator; it is the observation that the same operator applied from the opponent's perspective generates the defensive measures.

*Step 5 (Termination).* Can we push deeper? $T^(-2)$ asks: 'is there a move that guarantees I can create a fork regardless of the opponent's response?' If such positions existed, we would need a 6th measure. We check exhaustively: for every candidate position where fork_contrib $gt.eq 2$ after my move, does the opponent always have a spoiling response — either blocking one fork line or creating a forced threat that diverts me? The answer is yes: every candidate admits a spoil. Therefore $T^(-2) = emptyset$ and the iteration terminates. Five measures are provably sufficient.

*Step 6 (Residual).* When none of the dynamic measures (win, block, fork, opp_fork) distinguishes between candidate moves — all are zero or tied — a tiebreaker is needed. Density (the number of winning lines passing through a cell) is a static topological property that requires no Bellman reasoning. It is the 'when nothing urgent is happening, prefer cells with more strategic potential' measure. It exists at level 0 — it does not come from the Bellman iteration but from the mask geometry directly.

*Step 7 (Priority synthesis).* Given the 5 measures, what is the correct ordering? We identify critical positions — game states where choosing the wrong priority leads to a loss against perfect play. Each critical position generates a constraint: 'at this board, measure $X$ must dominate measure $Y$.' We feed these constraints to Z3. The satisfying assignment is unique: win $>$ block $>$ fork $>$ opp_fork $>$ density. No other ordering satisfies all critical-position constraints simultaneously. The priority ordering is a theorem, not a design choice.

*Step 8 (Verification).* The compiled feedback law (the priority ordering applied to the 5 measures) is executed against every reachable opponent response. A minimax oracle generates all legal opponent continuations — 549 distinct sequences when playing first. Result: 0 losses. The law achieves the game-theoretic optimum (draws against perfect play, wins against imperfect play) without ever having searched the game tree during its derivation.")

define subsec_inputs = ArxivSubsection("What Is Given vs. What Is Derived",
"The _only_ inputs to the system are:
+ The game exists on a $3 times 3$ grid (topology)
+ Three collinear cells constitute a win (the rule)
+ Players alternate single moves (alternation)

Everything else — the 8 masks, the 5 measures, the termination proof, the priority ordering, the feedback law, and the verified safety of the resulting play — is _derived_ by the pipeline. The human contribution is stating the game rules and invoking the machinery. No strategic insight, no heuristic, no training data enters at any stage.

The philosophical point: the strategy was always _latent_ in the rules. The pipeline's role is extraction, not invention.")

// =============================================================================
// Section 7: The Skolem Function Interpretation
// =============================================================================

define sec_skolem = ArxivSection("The Skolem Function Interpretation",
"The derivation chain of Section 6 has a precise logical reading that motivated the entire project. A two-player game with perfect information has the logical structure:

$ forall s_1 in O: exists r_1 in X: forall s_2 in O: exists r_2 in X: dots \"(X does not lose)\" $

This alternating quantifier formula states: for every opponent move, there exists a response such that for every subsequent opponent move, there exists a response... and the game never reaches a losing state.

In mathematical logic, a _Skolem function_ is the constructive witness that eliminates an existential quantifier: given the universal prefix $forall s$, the Skolem function $f(s)$ produces the specific $r$ that satisfies the existential claim. A _strategy_ is exactly a Skolem function for the game's alternating-quantifier formula — it maps every opponent move to the response that maintains the safety invariant.

This observation was the conceptual origin of the project: if strategies are Skolem functions, then strategy _discovery_ is Skolem function _synthesis_. The question becomes: can we mechanically construct the Skolem witness from the game's rules without searching the game tree?

The answer developed in this paper is: yes, via Bellman pre-image iteration. The iteration discovers the _representation_ (the 5-measure basis) over which the Skolem function has a closed form. Once the representation is found, the Skolem function is simply the priority composition — a lookup table in measure space rather than a search through game-tree space. The creative step was finding the coordinates; the Skolem function in those coordinates is trivial.

The mature methodology thus mechanizes what began as a logical observation:

$ \"Skolem witness exists\" arrow.r^(\"Bellman pre-image\") \"Representation discovered\" arrow.r^(\"Z3 synthesis\") \"Skolem function compiled\" $

The name 'Skolem Constructor' is retained to emphasize the logical content: what game theorists call a 'strategy,' control engineers call a 'feedback law,' and logicians call a 'Skolem function' are one object viewed from three disciplines. The pipeline constructs it from rules alone.")

// =============================================================================
// Section 8: Bellman-Invariant Basis Discovery
// =============================================================================

define sec_bellman_repr = ArxivSection("Bellman-Invariant Basis Discovery",
"We now formalize the central theoretical object: the representation over which optimal play becomes closed-form. The preceding sections demonstrated the concrete derivation for Tic-Tac-Toe. This section provides the mathematical framework — grounding our construction in the classical dynamic programming literature of Bellman [9] and Bertsekas [10] — and showing how the representation is discovered mechanically via operator iteration.")

define subsec_bcr_def = ArxivSubsection("Definition: Bellman-Invariant Basis",
"In classical dynamic programming [9], the _Bellman equation_ expresses the value of a state recursively:

$ V(s) = max_a { r(s, a) + V(T(s, a)) } $

where $T(s, a)$ is the state transition. The optimal policy is $pi^*(s) = arg max_a { r(s, a) + V(T(s, a)) }$. In the continuous-time limit, this becomes the Hamilton-Jacobi-Bellman (HJB) partial differential equation [10]:

$ 0 = max_u { f(x, u) dot nabla V(x) + r(x, u) } $

whose solution $V(x)$ determines the feedback law $u^* = arg max_u { f(x, u) dot nabla V(x) + r(x, u) }$. In both settings, the value function $V$ IS the strategy — once $V$ is known, optimal action at any state requires only a local evaluation, not a trajectory computation.

The difficulty is that $V$ is defined over the full state space (all board positions, all system configurations). Our key contribution is identifying a _compressed representation_ — a mapping $R: S arrow Sigma$ from states to a low-dimensional measure space — such that the Bellman recursion closes in the compressed coordinates.

A representation $R$ is a _Bellman-invariant basis_ if it satisfies two conditions:

+ *Closure:* The dynamics stay inside $R$. After any legal move, the new measure values are computable from the old measure values plus the move — without unfolding to the raw state. Formally: there exists $overline(F)$ such that $R(\"apply\"(s, m)) = overline(F)(R(s), m)$ for all states $s$ and moves $m$.

+ *Sufficiency:* The value function factors through $R$. Positions with identical measure values have identical optimal actions. Formally: $R(s_1) = R(s_2) arrow.r.double pi^*(s_1) = pi^*(s_2)$.

A representation satisfying both conditions admits a _closed Bellman recursion_ in measure space:

$ V(sigma) = max_i { r(sigma, i) + V(overline(F)(sigma, i)) } $

where $sigma = R(s)$ is the measure-space state. The optimal policy becomes:

$ pi^*(sigma) = arg max_i { r(sigma, i) + V(overline(F)(sigma, i)) } $

This is the compressed dynamic programming equation. For Tic-Tac-Toe: the raw state space has $3^9 = 19,683$ possible board configurations; the measure space $sigma = (w, b, f, \"of\", d)$ has 5 dimensions with small integer ranges. The Bellman equation is solved in 5 dimensions instead of 19,683. This compression ratio — from exponential state space to bounded predicate space — is the content of the representation theorem.")

define subsec_bcr_discovery = ArxivSubsection("Discovery via Bellman Pre-Image Iteration",
"The representation is not designed by a human strategist. It is _constructed_ by iterating the Bellman pre-image operator on the terminal predicate:

+ *Seed (Level 0):* The terminal value predicate is 'can complete a winning line on this move.' This defines $\"win_contrib\"(i) = |{k : \"bit\"(W_k, i) = 1 and \"popcount\"(\"bit_and\"(\"my\", W_k)) = 2 and \"bit\"(\"their\", i) = 0}|$. This is the game's boundary condition — the analog of terminal payoff in dynamic programming.

+ *Bellman pre-image (Level 1):* The operator $T^(-1)$ asks: 'what must hold NOW to guarantee the terminal predicate NEXT, regardless of opponent response?' Since the opponent can block one threat per turn, guaranteeing a win requires two simultaneous threats with distinct targets. This yields $\"fork_contrib\"(i) >= 2$ — the pre-image is computed, not assumed.

+ *Player swap:* The opponent's winning threat is our loss. Applying the same measures from the opponent's perspective yields $\"block_contrib\"(i) = \"win_contrib\"(i, \"their\", \"my\")$ and $\"opp_fork_contrib\"(i) = \"fork_contrib\"(i, \"their\", \"my\")$. This is not a new level of iteration but a symmetry observation: the game is symmetric between players.

+ *Termination ($T^(-2) = emptyset$):* The next pre-image asks: 'can I guarantee a fork regardless of opponent response?' Exhaustive computation confirms: for every candidate position, the opponent has a spoiling move (either blocking a fork line or creating a forced threat). No position satisfies the $T^(-2)$ predicate. The iteration terminates.

+ *Residual (Level 0, topological):* When no dynamic measure distinguishes candidates, density — the number of winning lines through a cell — serves as tiebreaker. This is a static geometric property, not a Bellman pre-image.

The result for Tic-Tac-Toe: five measures constitute the Bellman-invariant basis — $w$ (win contribution), $b$ (block contribution), $f$ (fork contribution), $\"of\"$ (opponent fork contribution), and $d$ (density). Their completeness is proved by the termination of the pre-image chain ($T^(-2) = emptyset$); their minimality is confirmed by Z3 counterexamples when any measure is removed.

This is a _constructive_ discovery method: each measure is derived from the previous by a definite operator application. No candidate enumeration, no heuristic search over possible representations. The Bellman pre-image operator GENERATES the basis, and the termination proof certifies its completeness.")

define subsec_bcr_bellman = ArxivSubsection("Solving the Bellman Equation in Measure Space",
"With the Bellman-invariant basis established, the Bellman equation is stated and solved entirely in measure coordinates $sigma = (w, b, f, \"of\", d)$:

$ V(sigma) = cases(+1 & \"if\" w >= 1 quad \"(terminal: active player wins)\", -1 & \"if\" w = 0 and \"not blocking gives opponent\" w' >= 1, +1 & \"if\" w = 0 and b = 0 and f >= 2 quad \"(fork forces win in 2 plies)\", -1 & \"if\" w = 0 and b = 0 and f < 2 and \"of\" >= 2 and \"not preventing\", 0 & \"otherwise\" quad \"(draw with optimal play)\") $

The feedback law emerges as the _unique solution_ to this recurrence:

$ pi^*(sigma) = cases(
  \"play cell with\" w(i) >= 1 & \"(Rule 1: Win)\",
  \"play cell with\" b(i) >= 1 & \"(Rule 2: Block)\",
  \"play cell with\" f(i) >= 2 & \"(Rule 3: Fork)\",
  \"play opponent's fork cell\" j & \"(Rule 4: Prevent)\",
  \"play\" arg max d(i) & \"(Rule 5: Develop)\",
) $

Each rule is derived from the recurrence by a separate lemma:

+ *Lemma 1:* $w >= 1 arrow.r.double V = +1 = sup(V)$. No other move can exceed the maximum. (From: terminal value definition.)
+ *Lemma 2:* Not blocking gives $V = -1$ (opponent wins next ply); blocking gives $V >= 0$. Bellman's $max$ selects blocking. (From: minimax opponent rationality.)
+ *Lemma 3:* $f >= 2$ means two threats with distinct targets; the pigeonhole principle (2 targets, 1 response) forces $V = +1$ in 2 plies. (From: 2-ply unrolling + alternation.)
+ *Lemma 3b:* $\"of\" >= 2$ means the opponent can fork next turn. If not prevented: opponent plays the fork cell, creating two threats — by Lemma 3 (from their perspective), $V = +1$ for them $= -1$ for us. Preventing gives $V >= 0$. Bellman's $max$ selects prevention. (From: 3-ply unrolling + symmetric application of Lemma 3.)
+ *Lemma 4:* When no tactical resolution exists _at any depth_, $V = 0$ for all moves. Density maximizes future fork potential — the geometric measure of optionality.

The priority ordering was not postulated. It was _derived_ from the value ordering ($+1 > 0 > -1$) and the measure-space transitions. The Bellman recursion has been solved. Only the feedback law remains.

The critical methodological point: the 'otherwise $V = 0$' (Lemma 4) is not self-evident. It must be _verified_ — either algebraically (by proving no deeper unrolling yields additional non-zero cases) or empirically (by confirming the law never loses against a perfect opponent). For Tic-Tac-Toe, depth-3 unrolling (Lemma 3b) is the last non-trivial case; beyond depth 3, the state is sufficiently constrained that $V = 0$ holds provably.

The law is player-independent: both players apply the same function with swapped inputs ($\"my board\", \"their board\"$). It is memoryless: no history, no search frontier, no transposition table. It is a combinational circuit:

$ \"board bits\" arrow \"mask arithmetic\" arrow \"priority encoder\" arrow \"move\" $

This is the signature of a solved control problem. The dynamic programming has been compiled away.")

// =============================================================================
// Section 9: Discussion
// =============================================================================

define sec_discussion = ArxivSection("Discussion",
"")

define subsec_philosophy = ArxivSubsection("Strategy as Latent Structure",
"The results support a structuralist view of game-theoretic knowledge: strategies are not _invented_ through experience or _discovered_ through search — they are _derived_ from constraint geometry. The center's dominance was always a theorem of the 8 masks. The fork's unblockability was always a consequence of alternation meeting distinct-target geometry. No amount of play would add to what deduction provides; play merely instantiates what the proof already guarantees.

This echoes the Aristotelian distinction between _dynamis_ (potentiality) and _entelecheia_ (actuality): the strategy exists in potentia within the rules and is actualized by the solver. The solver's role is analogous to a mathematician's — not creating truth but revealing it.

The implications extend beyond games. Any system with formal rules — protocol specifications, business logic, control systems — contains latent strategic structure derivable by the same methodology: encode the rules as constraints, pose structural questions, let the solver prove theorems.")

define subsec_hjb = ArxivSubsection("Strategy as Feedback Control Law",
"The feedback law derived in Section 8 is not merely a move table — it is a _control law_ in the sense of optimal control theory. This connects our work to the Hamilton-Jacobi-Bellman (HJB) framework, revealing a deep structural correspondence.

In continuous optimal control, the HJB equation determines a value function $V(x)$, and the optimal feedback law is:
$ u^*(x) = arg min_u H(x, u, nabla V(x)) $

The control law is _read off_ from the value function's gradient — no trajectory search required. The structure of $V$ determines the action at every state.

Our construction is the discrete game-theoretic analog. The Bellman-invariant basis $sigma = (w, b, f, \"of\", d)$ plays the role of $V$: it encodes the structural landscape of the game. The priority composition plays the role of the gradient: it extracts the optimal action from the local measure values. Just as $u^*$ in HJB is determined without simulating forward trajectories, our feedback law is determined without searching the game tree.

The parallel extends further. In HJB, the value function satisfies a PDE whose boundary conditions are the terminal payoffs. In our framework, the measures satisfy algebraic relations whose boundary conditions are the winning masks. Both are static objects (a PDE solution, a set of arithmetic theorems) that fully encode the optimal dynamic behavior.

The verification follows the same logic. In optimal control, the _verification theorem_ states: if $V$ satisfies the HJB PDE and the boundary conditions, then $V$ is optimal and $u^*$ is the optimal control. In our framework: if the feedback law produces 0 losses across all 549 reachable opponent sequences, then it IS the optimal strategy. Satisfying the safety invariant IS the proof — precisely as satisfying the HJB PDE is the proof in continuous control.

Strategy, in this framing, is not a sequence of decisions. It is a _mathematical object_ — a feedback law — that maps every reachable state to the action determined by the constraint geometry. The same object that control engineers call $u^*$, game theorists call a 'strategy,' and logicians call a 'Skolem function.' They are one thing, viewed from three disciplines.")

define subsec_knowledge = ArxivSubsection("Knowledge as Bellman-Compatible Compression",
"The pipeline exhibited in this paper — terminal predicate $arrow$ Bellman pre-image iteration $arrow$ measure basis $arrow$ Z3 synthesis $arrow$ feedback law — is an instance of a more general process. We claim:

_Useful domain knowledge corresponds to the discovery of Bellman-compatible representations._

To 'know' a domain, in the operative sense of being able to act optimally within it, is to possess a representation that (a) closes under the domain's dynamics and (b) is sufficient to determine the optimal action. The search for such representations is the creative step; their exploitation is mechanical.

This perspective recasts several established ideas:
+ *Feature engineering in machine learning:* The practitioner's art of choosing 'the right features' is the intuitive search for Bellman-compatible representations. Our pipeline mechanizes that intuition via operator iteration.
+ *Physical insight in science:* Conserved quantities (energy, momentum) are exactly the measures over which Hamiltonian dynamics close. Their discovery IS the physics; the subsequent calculation is deduction.
+ *Abstraction in software engineering:* A well-chosen interface hides implementation details while preserving the information needed for correct composition. This IS closure + sufficiency.

The approach does not claim to solve intelligence. It claims to _characterize_ one form of mechanizable knowledge creation: the constructive generation of representations via Bellman pre-images, and the certification of completeness via termination proofs. This is a strong enough claim and one the Tic-Tac-Toe example actually supports — the measures were generated, certified, and verified without human strategic intuition at any stage.")

define subsec_scaling = ArxivSubsection("Scaling Considerations",
"Tic-Tac-Toe uses 9-bit boards and 8 masks. Chess uses 64-bit boards and substantially more complex piece-movement rules. The methodology scales in principle: the strategic questions (which squares have maximum influence? which configurations are unblockable?) are the same. The practical challenge is that 64-bit arithmetic produces larger SMT formulas and the game tree has $10^{44}$ positions rather than $10^3$.

However, the key insight survives: _strategies_ scale differently than _solutions_. Enumerating all chess positions is intractable, but proving that 'a rook on an open file controls more squares than a rook on a closed file' is a bounded geometric fact about piece mobility masks — analogous to our density theorem. The derivation of such principles from chess rules via SMT is a natural next step.")

define subsec_thimbles = ArxivSubsection("The Picard-Lefschetz Connection",
"The pipeline of this paper — constraint-induced representation discovery followed by algebraic collapse — has a precise structural parallel in quantum field theory: the Picard-Lefschetz decomposition of oscillatory integrals.

In the Picard-Lefschetz framework, one starts with an enormous path space $cal(P)$ over which a path integral $Z = integral_(cal(P)) e^(i S[phi]) cal(D) phi$ is defined. Direct evaluation is intractable. The action functional $S$ determines critical points (saddle points in complexified field space), and from each critical point grows a _Lefschetz thimble_ $cal(J)_k$ — a steepest-descent manifold along which the integrand is maximally damped. The path integral then decomposes:

$ Z = sum_k n_k integral_(cal(J)_k) e^(i S[phi]) cal(D) phi $

where the $n_k$ are intersection numbers determined by the topology of the action's critical set. The enormous path space has been replaced by a finite sum over thimbles. The physicist does not invent the thimbles — the action determines them.

The structural correspondence with our methodology is:

$ cal(P) \"(path space)\" arrow.l.r.double \"Position space\" $
$ S \"(action functional)\" arrow.l.r.double \"Game rules (Bellman operator)\" $
$ {cal(J)_k} \"(Lefschetz thimbles)\" arrow.l.r.double {w, b, f, \"of\", d} \"(Bellman-invariant measures)\" $
$ \"Stationary phase structure\" arrow.l.r.double \"Bellman closure structure\" $
$ Z = sum n_k Z_k \"(thimble decomposition)\" arrow.l.r.double pi^* = \"priority\"(w, b, f, \"of\", d) \"(feedback law)\" $

In both cases:
+ The original space is too large for brute-force evaluation (all paths / all positions).
+ A generating operator (action / Bellman pre-image) produces candidate structures.
+ An admissibility condition (steepest descent / Bellman compatibility) selects the representations that compress the problem.
+ The result is a closed-form evaluation (thimble sum / feedback law) that replaces exhaustive integration (path sum / tree search).

Neither construction is brute force. Both are instances of: _discover the structure that makes brute force unnecessary_.

The parallel is not merely analogical. The measures in our construction ARE integrals — each measure $M(i) = sum_k P(\"mask\"_k, i, b_x, b_o)$ is a sum of a predicate over the constraint set (the 8 masks), just as a thimble integral sums the integrand along a topologically determined manifold. The masks play the role of critical points; the predicates play the role of the integrand; the Bellman-compatible measures play the role of the thimble integrals. The topology of the constraint geometry (which cells belong to which masks, how masks overlap and interact) is the analog of the Morse-theoretic structure that determines the thimble decomposition.

This suggests a unifying principle: _a Bellman-compatible representation is to optimal control what a Lefschetz thimble decomposition is to an oscillatory integral_ — both are constraint-induced compressions that transform intractable global computations into closed algebraic evaluations. The underlying meta-pattern is:

$ \"Huge space\" arrow.r \"Constraint-induced representation\" arrow.r \"Compressed recursion\" arrow.r \"Closed-form evaluation\" $

This pattern appears independently across mathematics, physics, and decision theory. Its recurrence suggests it is not domain-specific but reflects something fundamental about the relationship between structure and tractability.")

define subsec_generating = ArxivSubsection("The Generating Structure",
"The deepest reading of this work is not about games, control, or optimization. It is about what constitutes the _primary object_ in a formal system.

In each domain where this methodology applies, the same pattern emerges: what practitioners treat as the primary object (the solution, the strategy, the trajectory, the amplitude) is in fact a _derived_ object — a shadow cast by a deeper generating structure:

+ In game theory: the strategy is derived from the Bellman-compatible representation of the constraint geometry.
+ In optimal control: the feedback law $u^*$ is derived from the value function $V$.
+ In quantum field theory: the observable amplitude is derived from the thimble structure and intersection numbers.
+ In SAT solving: the satisfying assignment is derived from the clause geometry.

The solution was never the fundamental object. The _representation that generates it_ was.

This has a direct linguistic consequence. In the Kleis language, the primary construct is `structure` — not `function`, not `algorithm`, not `procedure`. A Kleis program defines generating structures (axioms, constraints, types); solutions follow as theorems. This is not a syntax choice — it is an ontological commitment: the generating object is primary, and the derived object (strategy, amplitude, feedback law) is a consequence that the language's verification backend extracts automatically.

Intelligence, in this framing, is not the ability to find solutions. It is the ability to _discover representations over which optimal decision-making becomes closed and tractable_. Once the representation is found, the passage from structure to solution is mechanical — a priority composition, a gradient, a projection. The creative act is recognizing that 5 measures generated from 8 masks suffice to close the Bellman equation, or that a value function generates all optimal trajectories, or that a set of thimbles generates all scattering amplitudes. Everything after that recognition is deduction.

The pipeline of this paper mechanizes part of that creative act: the Bellman pre-image operator generates the measures; the termination proof certifies minimality. What remains unmechanized is the choice of iteration seed and the base set of primitives — the 'axiom set' of the generation process. That choice corresponds to the physicist's selection of fundamental variables and the mathematician's choice of definitions. It is the last fortress of human insight in the pipeline.")

define subsec_symmetry = ArxivSubsection("Why Symmetry Did Not Drive Discovery",
"An initial intuition — drawing on Noether's theorem — suggested that the grid's $D_4$ symmetry group (8 elements: 4 rotations, 4 reflections) would be the key to discovering strategic invariants. Noether's theorem states that every continuous symmetry of a Lagrangian implies a conserved quantity. Perhaps discrete symmetries would yield analogous strategic invariants?

In the event, symmetry played no role in the discovery pipeline. The Bellman pre-image iteration — which actually produced the 5 measures — never invokes $D_4$. The reason is structural:

+ _Symmetry compresses state space; Bellman pre-images generate predicate space._ D4 tells us 'position A is equivalent to position B under rotation.' This is useful when enumerating positions (verification, game-tree search). But our method never enumerates positions during discovery. It operates on predicates defined over ALL positions simultaneously.

+ _The measures are D4-invariant by construction, without invoking D4._ Each measure is a sum over all 8 masks: $\"win_contrib\"(i) = sum_k f(W_k, i, b)$. Summing over all masks is invariant under any permutation that maps masks to masks — which is exactly what $D_4$ does to the grid. The symmetry is present in the result but was never needed as a derivation tool.

+ _Noether's theorem requires continuous symmetry and a Lagrangian._ Our game is discrete, finite, and has no conserved quantities in the physical sense. Moves change the board; nothing is 'conserved across turns.' The intuition from physics does not transfer to combinatorial games.

+ _The strategic content comes from the rules, not the geometry._ The Bellman pre-image asks: 'what structural property guarantees achieving the terminal predicate?' This depends on what constitutes winning (line completion) and how moves work (alternation, single-bit placement). An asymmetric game with irregular winning configurations — no rotational symmetry at all — would yield perfectly good Bellman-compatible measures by the same iteration.

The deeper lesson: symmetry tells you which positions are _equivalent_; the Bellman operator tells you which predicates are _strategic_. These are orthogonal concerns. Symmetry would become essential if one needed to enumerate candidate measures (then $D_4$ would massively constrain the search). But constructive derivation via operator iteration bypasses that enumeration entirely — each measure is extracted directly from the previous level's predicate, not searched for among all possible functions.

The $D_4$ reduction does appear in verification (reducing 549 sequences to 96 representative positions for the Z3 safety check). There, symmetry plays its classical role: compressing an exhaustive check. But it did not participate in the creative step — the discovery of what to check.")

define subsec_vs_ml = ArxivSubsection("Comparison with Machine Learning Approaches",
"Neural network game players and SMT-derived strategies differ fundamentally in what they produce:

+ *Neural networks* produce a _policy_ (probability distribution over moves) trained from data. The policy is opaque, approximate, and not formally verified. It may have blind spots exploitable by adversarial play.

+ *SMT derivation* produces _theorems_ (proved structural facts) derived from rules. The theorems are transparent, exact, and formally verified. They cannot be 'fooled' because they are logical consequences of the rules themselves.

The tradeoff is generality vs. rigor. Neural approaches handle complex games where full formalization is impractical. SMT approaches provide mathematical certainty but require the game to be formally specified. For any game that _can_ be formalized — and all finite games can — the SMT approach produces stronger guarantees.")

// =============================================================================
// Section 11: Conclusion
// =============================================================================

define sec_conclusion = ArxivSection("Conclusion",
"The contribution of this paper is not an optimal Tic-Tac-Toe player. It is a _mechanizable theory of representation discovery_.

The central result: the Bellman pre-image operator, applied iteratively to a game's terminal predicate, generates the minimal set of measures over which optimal play becomes a closed-form algebraic function. The iteration terminates at bounded depth — certified by exhaustive computation — and the resulting basis satisfies both closure (measures compose under dynamics) and sufficiency (they determine the optimal action at every reachable state). This is:

$ \"Terminal predicate\" arrow.r \"Bellman pre-images\" arrow.r \"Invariant basis\" arrow.r \"SMT synthesis\" arrow.r \"Feedback Law\" $

The pipeline requires no game-tree search to derive the controller. Z3 searches constraint space; the termination proof enumerates candidate positions in predicate space. But neither operation scales with the game tree — they scale with the _iteration depth_ of the Bellman pre-image operator, which for Tic-Tac-Toe is 1. The game tree has 255,168 terminal nodes; the representation has 5 dimensions. That compression ratio is not an implementation trick — it is the content of the representation theorem.

What the pipeline produces, concretely:

+ *Five measures* generated by operator iteration (win, fork at depth 1; block, prevent by player swap; density as residual). No human strategic input at any stage.
+ *A termination proof* establishing that no deeper pre-image yields actionable advantage — every depth-2 candidate admits a spoiling response.
+ *A priority ordering* synthesized by Z3 from critical-position constraints: the unique satisfying assignment that maps the basis to Bellman-optimal play.
+ *A compiled controller*: a memoryless combinational circuit — board bits $arrow$ mask arithmetic $arrow$ priority encoder $arrow$ move. The dynamic programming has been compiled away.

Verification: 0 losses across all 549 reachable opponent-move sequences against a perfect minimax player. The safety invariant holds at all 96 symmetry-reduced positions by Z3 ground-arithmetic proof.

The thesis: what appears to be strategic intelligence — the ability to play a game well — decomposes into (a) an operator iteration that discovers the right coordinates, and (b) deduction in those coordinates. Step (a) is the creative act, mechanized here by Bellman pre-images. Step (b) is algebra. The search tree was never the fundamental object; it was one method for computing a controller that has a closed form once the right basis is found.

The executable source code (8 files, 119 Z3-verified examples, all passing) serves as both the appendix and a reproducible artifact. The Kleis language and Z3 backend are available at https://kleis.io.")

// =============================================================================
// References
// =============================================================================

define ref_alphazero = ArxivReference("silver2018",
    "Silver, D. et al. A general reinforcement learning algorithm that masters chess, shogi, and Go through self-play. Science 362(6419), 1140-1144. 2018.")

define ref_kleis = ArxivReference("atik2026",
    "Atik, E. Kleis: A Formal Verification Language for Knowledge Production. https://kleis.io, 2026.")

define ref_heule = ArxivReference("heule2016",
    "Heule, M. J. H., Kullmann, O., and Marek, V. W. Solving and verifying the boolean Pythagorean Triples problem via Cube-and-Conquer. SAT 2016.")

define ref_konev = ArxivReference("konev2014",
    "Konev, B. and Lisitsa, A. A SAT attack on the Erdős discrepancy conjecture. SAT 2014.")

define ref_synthesis = ArxivReference("alur2013",
    "Alur, R. et al. Syntax-guided synthesis. FMCAD 2013.")

define ref_cegis = ArxivReference("solar2006",
    "Solar-Lezama, A. et al. Combinatorial sketching for finite programs. ASPLOS 2006.")

define ref_z3 = ArxivReference("demoura2008",
    "de Moura, L. and Bjørner, N. Z3: An efficient SMT solver. TACAS 2008.")

define ref_minimax = ArxivReference("vonneumann1928",
    "von Neumann, J. Zur Theorie der Gesellschaftsspiele. Mathematische Annalen 100, 295-320. 1928.")

define ref_bellman = ArxivReference("bellman1957",
    "Bellman, R. Dynamic Programming. Princeton University Press, Princeton, NJ. 1957.")

define ref_bertsekas = ArxivReference("bertsekas2017",
    "Bertsekas, D. P. Dynamic Programming and Optimal Control, Vol. I. 4th ed., Athena Scientific. 2017.")

define ref_schut = ArxivReference("schut2025",
    "Schut, L. et al. Bridging the human-AI knowledge gap through concept discovery and transfer in AlphaZero. Proceedings of the National Academy of Sciences 122(3), e2406675122. 2025.")

define ref_bloem = ArxivReference("bloem2018",
    "Bloem, R. et al. Graph games and reactive synthesis. In: Handbook of Model Checking, pp. 921-962. Springer. 2018.")

define ref_bansal = ArxivReference("bansal2023",
    "Bansal, S. et al. Towards efficient controller synthesis techniques for logical LTL games. arXiv:2306.02427. 2023.")

// =============================================================================
// Appendix
// =============================================================================

define appendix_source = ArxivAppendix("A", "Executable Source Code",
"The complete executable appendix consists of eight source files, each corresponding to a stage of the pipeline:

+ `tictactoe_rules.kleis` — Game specification: 27 axioms defining board, moves, and win condition (208 lines)
+ `tictactoe_topology.kleis` — Mask derivation from grid coordinates (203 lines)
+ `ttt_krylov.kleis` — Bellman pre-image iteration: measure discovery via operator application (329 lines)
+ `ttt_synthesis.kleis` — Z3 synthesis of priority ordering and thresholds (164 lines)
+ `tictactoe_bellman.kleis` — Bellman derivation of the complete feedback law (518 lines)
+ `tictactoe_complete_proof.kleis` — 96-node safety verification under $D_4$ reduction (1191 lines)
+ `ttt_match/prove_t2_empty.py` — Computational proof that $T^(-2)(\"win\") = emptyset$ (210 lines)
+ `ttt_match/ttt_match.py` — Match runner: Kleis feedback law vs perfect minimax engine (202 lines)

To reproduce all results:
```
kleis test examples/games/tictactoe_topology.kleis      # 11/11 pass, ~28s
kleis test examples/games/ttt_krylov.kleis              # 3/3 pass, ~23s
kleis test examples/games/ttt_synthesis.kleis           # 2/2 pass, ~23s
kleis test examples/games/tictactoe_bellman.kleis       # 7/7 pass, ~33s
kleis test examples/games/tictactoe_complete_proof.kleis # 96/96 pass, ~105s
python examples/games/ttt_match/prove_t2_empty.py       # T⁻² termination
python examples/games/ttt_match/ttt_match.py            # 0 losses vs minimax
```

Total verification time: approximately 3.5 minutes on a single core (Apple M-series). All source files are available at https://kleis.io under `examples/games/`.")

// =============================================================================
// Assemble Paper
// =============================================================================

define all_elements = [
    sec_intro,
    sec_related,
    sec_specification, subsec_board, subsec_bitops, subsec_winmasks,
    sec_derivation, subsec_density, subsec_independence, subsec_fork, subsec_prevention, subsec_hierarchy,
    sec_verification, subsec_tree, table_tree, subsec_invariant,
    sec_chain, table_chain, subsec_derivation_logic, subsec_inputs,
    sec_skolem,
    sec_bellman_repr, subsec_bcr_def, subsec_bcr_discovery, subsec_bcr_bellman,
    sec_discussion, subsec_philosophy, subsec_hjb, subsec_knowledge, subsec_thimbles, subsec_generating, subsec_symmetry, subsec_scaling, subsec_vs_ml,
    sec_conclusion,
    ref_alphazero, ref_kleis, ref_heule, ref_konev, ref_synthesis, ref_cegis, ref_z3, ref_minimax, ref_bellman, ref_bertsekas, ref_schut, ref_bloem, ref_bansal,
    appendix_source
]

define my_paper = arxiv_paper(
    paper_title,
    paper_authors,
    paper_affiliations,
    paper_abstract,
    paper_keywords,
    all_elements
)

example "compile" {
    let typst_output = compile_arxiv_paper(my_paper) in
    out(typst_raw(typst_output))
}

example "validate" {
    assert(valid_arxiv_paper(my_paper) = true)
    out("Paper is valid!")
}