The truth lives at the seam¶

Vitaly Reznik

Each electron has a property called spin. You can picture it as a tiny arrow; when you measure it along some direction in space, the answer is always one of two: "up" or "down".

Take two particles prepared together in a particular way, and send them apart. Ask about the pair: "are their two arrows opposite?" The answer is yes, every time. Now ask about one particle alone: "is the first one up?" There is no answer to be had in advance. Measure it, and you get "up" half the time and "down" half the time. The same for the second particle. The same if you measure along a different direction.

So the pair as a whole has a definite property that neither particle has. That is entanglement. Nothing on this page is new physics. What I want to show is what it looks like through the eyes of logic, and that this is not only a picture: it has been checked by a machine, step by step, and it has been run on a quantum computer.

Some claims below are marked proved: they are theorems checked in Lean 4, a program in which a machine verifies every step of a proof; their names are listed at the end. Some are marked computed: worked out by a program on a computer. Some are marked measured: numbers from the quantum computer. The rest is my reading.

A rule nobody notices¶

Here is a rule of ordinary reasoning so obvious that it has no everyday name:

If "A or B" is true, then A is true or B is true.

If "the key is in the drawer or in my coat" is true, then the key is in the drawer, or it is in my coat. A true "or" must have a true side. Logicians call this the cover property of "or".

ZTL (Zero-Trust Logic), the logic this site is about, keeps this rule: its "or" is true exactly when one side is true. It pays for that elsewhere: in ZTL, "A or not A" is not always true. (Proved.)

What "true" means for a quantum particle¶

Quantum theory describes a particle by its state. Think of all the possible states as a space. A yes/no question — "is the spin up?" — marks off a zone of that space (mathematically, a subspace). A statement is true of a state when the state falls entirely inside the zone: then measuring will give "yes" with certainty. If the state is only partly inside, the statement is neither true nor false of it, and measuring gives "yes" only with some probability.

In everyday logic, "A or B" covers exactly the cases of A together with the cases of B. In quantum theory, "A or B" is the smallest zone that contains both zones — and that can be more than the two put together.

This already breaks the rule for a single particle. For a particle whose spin points sideways, "up or down" is true — the two zones together fill the whole space of that spin — yet neither "up" nor "down" is true. This has been known since quantum logic was founded (Birkhoff and von Neumann, 1936). The pair does something stronger.

The pair¶

The two particles are in the state physicists call the singlet. Write u for up and d for down, first particle first. The singlet is a superposition — not a mixture, but a single combined state — of "u, d" and "d, u", in equal measure, with a minus sign between them. It contains no part where both arrows point the same way.

Ask the questions one by one.

About the pair: "the arrows are opposite", that is, "u, d — or — d, u". The singlet falls inside this zone. True. (Proved.)
Each side alone: "u, d"? "d, u"? The singlet falls inside neither. (Proved.)
About the first particle alone: "up"? "down"? Neither is true. (Proved.)
About the second particle alone: "up"? "down"? Neither. (Proved.)

Together: a statement about the whole pair is true, while no statement about either particle alone is true — not "up", not "down", for either of them. For one particle, the "or" lost its true side, but the particle still had its own true statement ("up or down"). Here the true statement belongs to the pair, and about either part on its own nothing is true beyond the empty "up or down", which is true of every particle whatever its state. The truth is at the joint between the two.

What exactly the machine checked: the singlet written as a list of four whole numbers, the questions written as zones spanned by whole-number lists, and "true" written as "falls inside the zone". No square roots, no approximation, and no axioms beyond Lean's core. The proof is for the up/down direction. For two other directions (left/right and front/back) the same was computed numerically: every up/down question about a single particle comes out at one half.

Where the truth went¶

My reading. The truth did not disappear. It belongs to the pair as a whole and is not divided between the parts. There is no half-truth sitting in each particle, waiting to be added up. That is what I mean by "it lives at the seam".

The same answers a question I had: when the first particle turns out up and the second down, where was the balance of spin before anyone looked? Not split between the particles. "The arrows are opposite" was true of the pair all along; it is asking each particle separately that finds nothing in either one.

Not what we expected¶

Two guesses, written down before the computations, were wrong. I keep them here because a check that never surprises you is not checking much.

The first guess was that the pair's statements could not even be built from statements about single particles, by combining them with "and" and "or". They can: combining single-particle zones does reach the singlet. What fails is not the ability to build the statement but its truth: the truth of the whole is not worked out from the truth of the parts. (Computed.)
I expected "not not A" to differ from A, because in ZTL it does. In quantum logic it does not — that is a known theorem, and the computation agreed on every statement it reached. My reading: quantum logic and ZTL give up different rules; they are not copies of one another.

On a real quantum computer¶

A theorem about lists of numbers is one thing. So the claims were turned into numbers and run on a real device: an IBM quantum computer, ibm_fez, with 156 quantum bits (qubits), on 19 July 2026. The pair was prepared and measured 4,096 times in one direction, and 4,096 times in a second direction at right angles to the first. (Measured.)

Each number is the fraction of the 4,096 runs in which the answer was "yes". Ideally the pair would give 1 and every question about a single particle would give 0.5.

question	first direction	second direction
the pair: are the arrows opposite?	0.951	0.958
one side of that "or"	0.475	0.491
the other side	0.476	0.467
first particle: up?	0.503	0.493
second particle: up?	0.504	0.517

With 4,096 runs, each number is uncertain by about ±0.008, and each direction was run once. Why two directions? In the first direction alone, a much more ordinary pair — one that is secretly either "u, d" or "d, u", decided in advance — would give the same numbers. The second direction tells them apart: only an entangled pair stays opposite there too.

The results are consistent with the theorem: the pair comes out opposite about 95% of the time, and the single particles come out near one half. The missing 5% are most likely the machine's own imperfections (the state decays a little, and the readout makes errors); this was not tested separately. One number, 0.467, is about four uncertainties away from one half, which points to a small bias of the device in that run.

So the truth at the seam, measured on a real machine, also comes with a margin of error.

What is old, and what this page adds¶

The physics is old. Einstein, Podolsky and Rosen raised the puzzle in 1935; the spin version used here is David Bohm's (1951); John Bell (1964) showed that no account in which each particle carries its own answers can reproduce the quantum predictions. That the quantum "or" can be true with no true side follows from Birkhoff and von Neumann's quantum logic (1936).

What this page adds is narrow: the statement for the singlet — a true statement about the pair, none about either part — checked by machine in whole numbers; and the same claims run on hardware, with the program published so that anyone can repeat it.

In short: a whole can have a true property that none of its parts has, and here that has been checked step by step.

How to check¶

All files are in the open repository inventor1975/ZTL.

The proofs: lean/JunctionWitness.lean — pair_true, disjunct_ud_fails, disjunct_du_fails, spin1_up_fails, spin1_down_fails, spin2_up_fails, spin2_down_fails, and junction, which combines them. ZTL's rule for "or": cover_or_T in lean/ZTL.lean; that "A or not A" can fail in ZTL: lem_needs_ground, same file.
The computations along other directions and the two wrong guesses: dilemmas/quantum_pair.py.
The hardware run: dilemmas/quantum_junction_hw.py. It runs on a simulator with --sim, or on IBM hardware with your own IBM account and --ibm. The two IBM job numbers of the run above are recorded in the file. (A reader of this page found that the program had the two particles' labels swapped; that was corrected on 30 October 2026. The counts did not change.)