The Meeting Game

A lone table has two lines, and nothing in the rules says how likely each one is. The game has no dice.

Let P meet a detector particle M. Now the joint table has two lines, P's 0 with M's 0 and P's 1 with M's 1: a promise. Nothing is written.

Try this. P secretly swaps its two lines. Can M, touching only its own table, put everything back? M has two moves. It can swap its own labels, which puts every arrow back in its old cell. And it can turn the arrows: each cell has a different M label, so M has a handle on each arrow and can turn each one by its own angle. Turning only rotates; it never stretches.

M can undo P's swap exactly when the two lines have the same length. Then the swap changed nothing that P's side could ever notice, so the two lines must have the same odds. That is a theorem, not a rule we put in. A wrong direction (a phase) is repaired by M's turn. A wrong length is not: nothing on M's side can stretch.

Before the meeting there is nobody to undo anything. A lone table gets only what symmetry forces: equal odds when nothing tells its lines apart, and never odds from its lengths. The lengths become odds once a counterparty holds the other side.

Unequal lines fail room 1's test. So zoom in on M. M has more inside than its two labels show. Up close, its label "0" is really several finer labels, and so is "1", and we can read them so that every cell has the same length. Nothing is added and nothing new meets P: this is only a closer description of M's side. One part of M keeps a note of each fine label, so every cell has a counterparty of its own, inside M.

Now any two cells pass room 1's test, even two cells from different lines. All cells are interchangeable, so all cells have the same odds.

Read the table as in room 1: P down the side, M across the top, an arrow wherever the two match. P's side does not change: P still has two lines. Only M's side gets finer, because up close M tells its cells apart: "0" is 0a, 0b, 0c. In brackets are Zurek's names: s for P's lines, ε for M's labels, c for M's fine labels, which he calls a counter, a part of M. He counts from 1.

Different labels mean perpendicular cells. M can tell 0a from 0b for certain, so looking at one gives no trace of the other: their overlap is 0, and zero overlap is what a right angle means. The grid under the cells shows the overlaps.

Two separate steps; keep them apart.
1. Geometry, only arithmetic. Perpendicular pieces add like the two short sides of a right triangle: their squared lengths add. Line 0 is n cells, each of length 1/√N, so its length squared is n × 1/N = n/N. The spiral under the cells draws it, one right angle per new cell.
2. Odds, the assumption. Every cell has the same odds, so a line that owns n of the N cells has odds n/N.
Put the two side by side and the odds equal the line's length squared. Nobody squared a length to get odds: the close look at M cut the promise into equal pieces, and the square is simply what the geometry says about n perpendicular pieces.

What is still assumed: odds belong to the side that holds them, do not care about names, and add over cells.

From those assumptions, cells over the total is a machine-checked proof (Lean 4, Mathlib) for whole-number cell counts. Other lengths need continuity, which no certificate covers.

In #17 we told this as a loop: pick, sign, refuse, pick again. Here is the version with no loop. When two holders meet, each makes one light touch: one event touches one line. Usually it lands nowhere. Sometimes it lands on a line, in proportion to that line's length. The darts below are the meetings where both touches landed somewhere.

Two touches are one dart on the square: P's across, M's up. The meeting only ever wrote the two matched blocks on the diagonal. A dart on the diagonal writes that line for every holder. A dart off it is a miss: nothing is written, and nothing is left behind. The next meeting of two holders throws again.

The written share is an area: length times length. It lands on room 2's cell count exactly. So two touches inside one meeting are one honest way for two sides, each seeing only its own lengths, to draw one of the equal cells.

A miss is exact, not a figure of speech. In the lines the meeting wrote, an off-diagonal pair has no cell at all, so nothing can ever be written there. And the number of misses before the write is the same on every table, so nobody learns anything by counting them.

Each side throws its own dart. What they share is not a dart but the cells that are missing. How much they share is one number, made only by a meeting and spent by the settlement.

How many books must agree? Two gives the cells. One gives the length law (no counterparty, room 1 says a lone table gets no odds from its lengths). Three or more is a vote, and the longer line wins everything: the telephone game.

P has met M: a promise. Now other particles meet M. Each such meeting is a look: the witness turns a little (the "look" dial) if M's line is 1. At 90° it is a perfect copy; at 0° it saw nothing.

Then somebody tries to undo everything: every meeting it can reach, last one first. It holds P and M, and the first few witnesses (the "undo reaches" dial). Afterwards we ask P's table: how much of the other line came back?

A crowd of direct looks: each direct witness left out of reach costs a factor cos(look), and the factors multiply. A chain, where each witness only hears from the one before, never gets past its first link. Evidence adds up; hearsay doesn't.

Both laws, and the chain's level line on the chart, are a machine-checked theorem (Lean 4, Mathlib) for every number of witnesses. One honest clause: it is proved for a line-by-line copy of the toy's code in Lean, which reproduces every number the toy ever stored; for looks between 0° and 90°.

This is the answer to #18's question. The detector's first touch is the same meeting as the marker's. The detector then talks to a crowd at once, and the crowd is out of reach. The marker was left alone.

Nothing here picks the line. The witnesses only make it permanent.