Keeler's Theorem: Body Swap Machine and Affine Transpositions

Table of Contents

;; The Prisoner of Benda (Futurama S07E10)
;; 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

A mind-swap machine operates on bodies [n]. Constraint: each unordered pair {a,b} swaps at most once, ever. After an arbitrary history of swaps producing permutation pi in S_n, restore the identity using two fresh bodies {x,y}.

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.1. 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. The body swap machine is the group-theoretic distillation of pipeline reversal under a resource constraint.

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/:

  1. Pick characters from Futurama (or add custom names)
  2. Perform swaps — drag-and-drop or click pairs. Each pair dims after use (affine: consumed).
  3. See the permutation — who is in whose body, cycle notation
  4. Click "Keeler Repair" — two fresh characters appear (Sweet Clyde, Bubblegum Tate). The repair swaps animate step-by-step.
  5. Verify — everyone is back. The trace is displayed as a pipeline (like the transform tool).

2.2. Architecture

Same stack as the transform tool:

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", S07E10)
  • Evans, Huang, Nguyen. "Mind switches in Futurama and Stargate." Amer. Math. Monthly 121 (2014) 136–144. arXiv:1204.6086
  • Elder, Vega. arXiv:1608.04809. p-cycle machine generalization.
  • No Mathlib/Lean formalization located as of 2026-06-10.

5. Related Work