Keeler's Theorem: Body Swap Machine and Affine Transpositions
Table of Contents
;; The Prisoner of Benda (Futurama 6ACV10)
;; Amy swaps with the Professor, then Bender, then...
;; The machine constraint: each pair swaps AT MOST ONCE.
;; After the mess: can everyone get back to their own body?
user=> (def cast [:amy :professor :bender :leela :fry :zoidberg :hermes])
user=> (-> (swap :amy :professor) ; Amy is in Professor's body
(swap :amy :bender) ; Amy (in Professor) swaps with Bender
(swap :leela :fry)) ; Leela and Fry swap
;; Result: a permutation no one knows how to undo...
;; ...until Keeler proves: introduce two fresh bodies, always fixable.
user=> (keeler-repair perm [:sweet-clyde :bubblegum-tate])
;; => everyone restored. QED.
Pick two character cards to swap. Each pair can only swap once (affine constraint). Two fresh Globetrotters repair everyone.
1. Problem Statement
Professor Farnsworth invents a machine that allows two people to switch minds. The catch: the machine cannot be used twice on the same pair of bodies. After a series of swaps, everyone is in the wrong body and the obvious fix — just swap back — is blocked by the machine's constraint. Can everyone be restored?
1.1. The budget
With n bodies, the number of unique pairs is n(n-1)/2. Each pair can
be used at most once. That is the total budget of swaps available:
| Bodies (n) | Unique pairs | Example |
|---|---|---|
| 2 | 1 | One swap, spent, stuck |
| 8 | 28 | Main cast |
| 12 | 66 | Example roster (9 episode + Scruffy, Nixon, Nikolai) |
| 14 | 91 | + Sweet Clyde and Bubblegum Tate |
With n=2, one swap exhausts the only pair. The two people are stuck in each other's bodies with no way back. That is the inciting incident of the episode — and the k=2 base case of the theorem.
1.2. The theorem
Keeler proved (on the show's blackboard) that introducing just two fresh people who have never swapped with anyone is always enough to fix everyone, no matter how tangled the swaps have become.
1.3. Formal statement
Keeler (2010, blackboard in "The Prisoner of Benda"):
For n >= 2, the inverse of any pi in S_n is a product of distinct transpositions in Sn+2 \ S_n.
The repair transpositions each move x or y. Distinctness from the
history that produced pi is therefore structural: history edges lie
in Sym2 [n], repair edges each touch {x,y}. No bookkeeping over
the history is required.
This is an affine resource discipline: each edge of Sym2 beta is a
consumable resource, used at most once across the entire trace
(history ++ repair).
1.4. Connection to the transform pipeline
The transform codec pipeline operates on the same structure. Each codec step is a function; an involution (like rot13) is a transposition in function space. The "reverse pipeline" is the inverse permutation. Both are symmetric group actions with a no-reuse constraint on transpositions.
| Transform pipeline | Body swap machine |
|---|---|
| codec step | transposition |
| involution (rot13) | swap (a,b) |
| reverse pipeline | permutation inverse |
| surjection (no inverse) | (no analog) |
| pipeline composition | trace product |
:d suffix (decode) |
repair swap |
2. The Interactive Tool
2.1. What it does
A browser-based body swap simulator at /tools/body-swap/:
The tool lets you build a permutation by clicking pairs, watch the cycle structure change, then run Keeler's repair step-by-step with two fresh Globetrotters. Each pair dims after use – the affine constraint is visible.
2.2. Architecture
ClojureScript + shadow-cljs, matching the transform tool's build:
| Layer | File | Role |
|---|---|---|
| ClojureScript | src/wal_sh/tools/body_swap/core.cljs |
Permutation engine |
| ClojureScript | src/wal_sh/tools/body_swap/browser.cljs |
DOM renderer |
| shadow-cljs | shadow-cljs.edn :tools-body-swap |
Build |
| Lean 4 | spec/keeler/Keeler.lean |
Formal proof |
| Dafny | spec/dafny/Keeler.dfy (optional) |
Compiled proof |
2.3. Core algorithm (Clojure)
The repair procedure for a single k-cycle (c_0 c_1 ... c_{k-1}):
(defn repair-cycle
"Keeler's blackboard formula for one cycle.
Returns a sequence of swaps using fresh bodies :x and :y."
[cycle]
(let [k (count cycle)]
(concat
;; swap x with each element except the last
(map (fn [c] #{:x c}) (butlast cycle))
;; swap y with the last, then x with the last, then y with the first
[#{:y (last cycle)}
#{:x (last cycle)}
#{:y (first cycle)}])))
(defn repair-permutation
"Apply Keeler's theorem: decompose into cycles, repair each.
Each cycle repair transposes x<->y. If odd number of cycles,
x and y end up swapped -- add a final [x y] to fix."
[perm x y]
(let [cycles (perm->cycles perm)
swaps (vec (mapcat #(repair-cycle % x y) cycles))
after (apply-swaps perm swaps)]
(if (= (get after x x) y)
(conj swaps [x y]) ;; parity correction
swaps)))
Each cycle repair leaves x and y transposed (always, regardless of
cycle length). After repairing all cycles: odd count of nontrivial
cycles means x and y are swapped, even means they are fixed. The
final [x y] swap corrects the parity.
2.4. Permutation engine
(defn swap
"Apply transposition {a,b} to permutation (as map)."
[perm a b]
(let [pa (get perm a a)
pb (get perm b b)]
(assoc perm a pb b pa)))
(defn perm->cycles
"Decompose permutation (as map) into disjoint cycles."
[perm]
(loop [remaining (set (keys perm))
cycles []]
(if (empty? remaining)
(filterv #(> (count %) 1) cycles) ; drop fixed points
(let [start (first remaining)
cycle (loop [current start acc []]
(let [acc (conj acc current)
next (get perm current current)]
(if (= next start) acc
(recur next acc))))]
(recur (reduce disj remaining cycle)
(conj cycles cycle))))))
(defn legal?
"Is the trace legal? Each pair used at most once."
[trace]
(apply distinct? trace))
3. Lean 4 Formalization
3.1. Encoding: alpha oplus Bool
Fresh bodies x : inr false=, y : inr true=. A repair swap
Equiv.swap (inr b) (inl a) is syntactically disjoint from any
history swap Equiv.swap (inl a) (inl a').
3.2. Key lemmas
| Lemma | Statement | Status |
|---|---|---|
repair_disjoint_history |
repair edges != history edges by constructor | skeleton |
cycle_repair |
per-cycle blackboard formula inverts the cycle | skeleton |
keeler |
weak form: exists legal repair trace for any pi | skeleton |
keeler_with_history |
strong form: joint nodup with history | skeleton |
3.3. Conjecture registry
| ID | Claim | Confidence |
|---|---|---|
| F1 | Existence provable in 600–800 LoC over Mathlib | probable |
| F2 | Distinctness is structural under oplus Bool |
theorem (constructor discrimination, one line) |
| F3 | Per-cycle formula verifies by list induction | provable (not cycle-type classification) |
| F4 | EHN optimality is >= 5x the cost of existence | speculative (sign-based lower bound) |
| F5 | Parity: x,y transposed iff odd number of nontrivial cycles | theorem (each cycle repair transposes x,y; induction on cycle count) |
4. Prior Art
- Keeler 2010, episode blackboard ("The Prisoner of Benda", 6ACV10)
- Evans, Huang, Nguyen. "Keeler's theorem and products of distinct transpositions." Amer. Math. Monthly 121 (2014) 136–144. arXiv:1204.6086
- Evans, Huang. "The Stargate switch." arXiv:1209.4991
- Elder, Vega. arXiv:1608.04809. k-cycle machine generalization (all k ≥ 2).
- No Mathlib/Lean formalization located as of 2026-06-10.
5. Related Work
- Transform pipeline spec — involutions and pipeline reversal
- Reversible pipeline transforms — the parent research
- Dafny–Clojure JVM Interop — verified codecs on the JVM
- Dafny 4.11.0 on FreeBSD — toolchain for compiled proofs