wal.sh
home > research > keeler-theorem-body-swap > spec · Jun 11, 2026

Keeler Mind-Swap Simulator: UI Requirements

Keeler Mind-Swap Simulator: UI Requirements

Table of Contents

1. Purpose

Requirements for rebuilding the body swap simulator from scratch in any language (ClojureScript, TypeScript, Rust/WASM, Lean 4 game, etc.). Same role as the transform tool spec — an implementing agent reads this and produces a working tool.

The current ClojureScript implementation at src/wal_sh/tools/body_swap/ is the reference. This spec extracts the requirements so another implementation can be verified against it.

2. Confirmation gate

Before writing code, the implementing agent MUST state:

  1. How many swappable bodies are in the cast (answer: 12)
  2. How many helpers (answer: 2, Sweet Clyde and Bubblegum Tate)
  3. What the affine constraint is (each pair swaps at most once)
  4. What the episode swap sequence produces (a 7-cycle and a 2-cycle)
  5. How many repair swaps the episode needs (answer: 13)

3. Domain model

Term Definition
body keyword identifier; holds exactly one mind
mind same identifier space; mind m is home iff held by body m
state map body -> mind; a bijection (permutation)
edge unordered pair of distinct bodies
trace ordered vector of edges
legal all trace edges pairwise distinct
helper :sweet-clyde or :bubblegum-tate; introduced only during repair

4. Invariants

  • U01 Affine edges: no edge appears twice in the trace
  • U02 Bijection: state is always a valid permutation
  • U03 Edge cap: trace length <= C(n,2) where n = body count
  • U04 Repair provenance: every repair swap touches a helper
  • U05 Helper freshness: no history swap touches a helper

5. Cast

Row Characters Swappable
1 Amy, Professor Farnsworth, Bender, Leela yes
2 Fry, Dr. Zoidberg, Hermes, Kif yes
3 Wash Bucket, Emperor Nikolai, Scruffy, Nixon's Head yes
4 Sweet Clyde, Bubblegum Tate no (helpers)

6. Episode swap sequence (Prisoner of Benda, S07E10)

# Swap Reason
1 Professor <-> Amy Prof wants youth, Amy wants to eat
2 Amy(Prof) <-> Bender Bender needs human body for heist
3 Professor(Amy) <-> Leela Leela wants movie discount
4 Amy(Bender) <-> Wash Bucket Bender needs to reach Nikolai
5 Fry <-> Zoidberg Fry tests if Leela likes his looks
6 Wash Bucket(Bender) <-> Nikolai Bender gets emperor's body
7 Leela(Amy) <-> Hermes Hermes thinks he can lose Amy's weight

Result: (professor leela hermes amy bender nikolai wash-bucket)(fry zoidberg)

Repair: 13 swaps via Sweet Clyde + Bubblegum Tate. Everyone restored.

7. Functional requirements

7.1. FR1 Configuration

  • Body count selector or fixed cast (12 characters)
  • Reset: identity state, empty trace, helpers removed

7.2. FR2 Manual swapping

  • Click two body cards to swap
  • Consumed edge: refused with message, state unchanged
  • Click selected card to deselect
  • Swapping disabled during repair animation

7.3. FR3 Scramble

  • Random legal history from fresh reset
  • Seedable for reproducibility

7.4. FR4 Keeler repair

  • Introduces helpers, computes repair plan, animates step by step
  • Plan per k-cycle [c0 ... c_{k-1}]: x<->c0, x<->c1, ..., x<->c_{k-2}, y<->c_{k-1}, x<->c_{k-1}, y<->c0
  • Final x<->y iff helpers end transposed (odd nontrivial cycle count)
  • Cards update live during animation

7.5. FR5 Verification

  • After repair: all bodies hold own mind, trace is legal
  • Failure is loud: names the residual permutation

7.6. FR6 Displays

  • Body cards: name, whose mind is inside, where own mind went
  • Cycle notation
  • Consumed edge list (struck through)
  • Repair trace with step highlighting

8. Test contract (property-based)

Property Conjecture Trials
Keeler restores identity for any legal trace F1 100+
Every repair swap touches a helper F2 100+
Parity: final x<->y iff odd cycle count F5 100+
All repair edges distinct (affine) U01 100+
Swap is involution — 200+
Trace is always legal U01 100+

Current test suite: 13 tests, 21 assertions, 600 PBT trials, 0 failures.

9. Chain grammar (if URL state is added)

swaps = edge ("+" edge)*
edge  = body "-" body
body  = [a-z][a-z0-9-]*

Same pattern as the transform tool: + is URL-encoded space, default split works after URL decode.

10. Non-functional

  • No network. Static bundle.
  • Deterministic given seed.
  • Home/displaced encoded by color AND glyph (accessibility).
  • Under 500KB gzipped.

11. Related