The Fredkin Machine

Conservative logic running on the QLF substrate — watch the ball count hold, the twist action stay at zero, and the whole computation run backwards. Fredkin_QLF.md · fredkin_qlf.py · QLF_Fredkin.lean

Built at the suggestion of Van Hovey.

The billiard collision — conservation of logic is conservation of balls
Two balls on crossing tracks. Present reads as 1, absent as 0. If both arrive they collide and leave on the two inner exits; otherwise each continues on its own outer one. Fredkin & Toffoli's interaction gate, and the primitive the circuits below are built from.
BALLS IN → OUT
00
conserved
SIGNED TWIST ACTION
(0, 0, 0, 0)
ZFA throughout the collision
INFORMATION DISCARDED
0 bit
the collision forgets nothing
BALLS ON THE WIRES
0 of 0 at the start
conserved
Fredkin's conserved quantity. A gate routes balls; it never makes or destroys one.
SIGNED TWIST ACTION
(0, 0, 0, 0)
ZFA — the history is realized
Each ball is the plaquette ^<v>. A gate permutes wires, so the multiset never changes — the vector cannot move off zero.
FREE-ENERGY LEDGER
0.000 nat
nothing forgotten yet
Every gate so far is a bijection, so nothing merged and nothing was forgotten. ΔF = −log 2 is the price of forgetting, and a permutation forgets nothing.
THE HISTORY, AS TWISTS
The whole register as one history: every wire carrying a ball contributes its plaquette. This is the string twist_core.is_zfa accepts.
WHEN THE BILL ARRIVES
Result wires (kept)
Garbage wires (discarded)
Cost to reset the garbage0 bit — 0.000 nat
On the count: garbage is every wire you decline to keep, which includes the spent input wires — the adder runs on 32 wires (3 inputs + 29 ancillas) and keeps 2, so 30 are garbage. fredkin_qlf.py reports 29 because it counts ancillas allocated. Same circuit, two honest accountings.
Running the machine is free. Tidying up is not: resetting k garbage wires to zero is a 2^k → 1 map, and that is the only place Landauer's quantum is charged. Keep the garbage and you owe nothing — which is Bennett's point, arrived at here from the one closure quantum rather than assumed beside it.