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, 6ACV10)

# 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

Buttons are grouped into three toolbar zones separated by visual dividers:

Group Buttons Purpose
Scenarios Scramble, Worst Case, Episode Generate swap histories
Proof Keeler Repair Demonstrate the theorem
Meta Reset, Share Admin: clear state, export URL

7.1. Scenarios

7.1.1. FR1 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.1.2. FR2 Scramble

  • Random legal history from fresh reset
  • URL updates with seed on completion

7.1.3. FR3 Worst case

  • Exhaust all C(12,2) = 66 pairs
  • Demonstrates maximum-entropy permutation

7.1.4. FR4 Load episode

  • Replay the 6ACV10 swap sequence (7 swaps)
  • Deterministic (no randomness)

7.2. Proof

7.2.1. FR5 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.2.2. FR6 Verification

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

7.3. Meta

7.3.1. FR7 Reset

  • Returns to identity state, empty trace, helpers waiting
  • Clears ?s= from URL

7.3.2. FR8 Share

  • Copies current URL (with ?s= seed) to clipboard
  • Flash confirmation on button

7.3.3. FR9 Seed loading

  • On page load, decode ?s= parameter and replay trace
  • Invalid seeds are silently ignored (falls through to idle)

7.4. Displays

7.4.1. FR10 Cards and indicators

  • 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. URL seed encoding

Shareable state via ?s=<base64url> query parameter. The address bar updates live on every action.

9.1. Encoding scheme

Each swap is packed into one byte: high nibble = cast index of first body, low nibble = cast index of second body. The byte sequence (preserving swap order) is base64url-encoded. 

cast indices:  0=amy 1=professor 2=bender 3=leela
               4=fry 5=zoidberg 6=hermes 7=kif
               8=wash-bucket 9=nikolai 10=scruffy 11=nixon

byte = (index-a << 4) | index-b
seed = base64url(byte-sequence)

Example: the episode sequence (7 swaps) encodes as ~12 characters. Worst case (66 swaps, all pairs) encodes as ~88 characters.

9.2. Round-trip property

decode(encode(trace)) = trace – the edge sequence and resulting permutation must be identical. This is testable as a PBT property.

9.3. URL lifecycle

  • Page load: if ?s= present, decode and replay trace.
  • Every action: replaceState with current seed (scramble, worst case, episode, card swap).
  • Reset: clears ?s= from URL.
  • Share button: copies current URL to clipboard.

10. UI state machine

ui-states.png

Figure 1: UI interaction states (derived from browser.cljs atom discriminants)

Six states, two interaction modalities (buttons and card clicks):

State Atom discriminant Entry
idle empty trace, no selection Reset, page load
seed_loaded transient page load with ?s=
has_trace edges > 0, no selection swap, scramble, worst, episode
char_selected selected non-nil card click
repairing repair non-nil, timer active Keeler Repair button
repaired repair done, timer cleared timer completes all steps

The affine_violation node is transient (console warning + deselect), not a durable state.

11. Non-functional

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

12. Related