What can these observations distinguish?

Suppose two records both begin with 0. Does that make them the same record? Follow a small example through the four information-escape questions, then bring the same questions to an observation of your own.

A fixed four-state model

Elementary educational enumeration — not a new Lean theorem or a certified judge run. Our entire state space is 00, 01, 10, 11. For a state ab, the first readout returns a and the second returns b. Two states are indistinguishable when every selected readout returns the same value on both.

Write E(S) for the escape pairs left by the selected readouts S. These are ordered pairs of distinct states: (00, 01) and (01, 00) both count; (00, 00) never counts. Each group below contains exactly the states that still look alike. Different groups are distinguishable. In the table, Groups lists these indistinguishable groups and Pairs counts the escape pairs.

Scroll sideways if needed. Keyboard: focus the table, then use Left/Right arrows.

A group of size k contributes k(k − 1) ordered distinct pairs: choose the first state in k ways, then a different state in k − 1 ways. Add over the groups. Thus no readouts leave 4 × 3 = 12 pairs; either coordinate alone leaves 2 × (2 × 1) = 4; both leave only singleton groups, hence 0.

Where did information escape?

With only first, 00 and 01 both return 0. The escape pairs are (00, 01), (01, 00), (10, 11) and (11, 10). The first coordinate says nothing about which second coordinate a state has.

How is that escape addressed?

Add second while keeping the same state space and the first readout. It returns 0 on 00 and 1 on 01, separating a pair that first alone could not distinguish. An extra readout supplies a distinction the old readout lacks. The source law escapePairs_insert describes this filtering: adding a readout retains only old escape pairs on which that readout also agrees.

What new information emerges?

The pair of observations now identifies each of these four states: 00 returns (0, 0), 01 returns (0, 1), 10 returns (1, 0) and 11 returns (1, 1). All four pairs left by first are distinguished by second. You can check each distinction directly in the table.

Where does information continue to escape?

First alone still confuses 10 with 11; second alone still confuses 00 with 10. With both, no distinct pair remains indistinguishable inside this fixed model. An empty residual here says nothing about unmodeled states, unmeasured properties or every question one could ask about the world.

What does each readout uniquely contribute?

Now fix one catalog C = {first, second}. For each entry i, remove only that entry and compare with the same full catalog. Its unique captures are E(C without i) minus E(C), as formalized by uniqueCapturePairs_eq_sdiff. Here E(C) is empty, so the exact sets are:

• first: (00, 10), (10, 00), (01, 11), (11, 01) — 4 pairs. Removing first leaves second, which confuses states within each of its two groups.
• second: (00, 01), (01, 00), (10, 11), (11, 10) — 4 pairs. Removing second leaves first, with the other two groups.

These counts answer a different question from a sequence of additions. Starting with no readouts, adding first removes 8 of the 12 pairs; adding second removes the remaining 4. The fixed-catalog unique counts are 4 and 4, not 8 and 4. Pairs differing in both coordinates — (00, 11), (11, 00), (01, 10) and (10, 01) — are distinguished by either readout. They belong to neither unique-capture set, so unique counts need not sum to 12.

Distinct catalog entries can even have the same agreement kernel: they distinguish exactly the same pairs. Then both have zero unique capture, by same_kernel_both_zero. This does not imply worthlessness; a distinction can be shared. These comparisons establish neither universal research value nor historical novelty.

Follow the source, keep the boundary

The EscapePairs source defines escapePairs and uniqueCapturePairs. Its coordinate fixture, escapeFixtureCatalog, uses Bool × Bool, represented above by two digits, and checks the empty full-catalog residual and the two unique counts of four.

That fixture’s units use Statement := True and proof := True.intro. They illustrate the kernels; they do not establish that a substantive theorem’s meaning is faithfully represented by a declared readout, or that it has been registered for the judge. In TheoremUnit, NativeTheoremUnit ties a proof to a law of a realization, while LegacyPrimitiveRealization requires an equivalence connecting a legacy statement to that law. Such semantic connections require their own evidence.

Read the EscapePairs Blueprint page in this snapshot.

The formal source links above are pinned to this book’s captured snapshot. Check the definitions and assumptions when carrying this example to another revision or context.

For operational status, follow the current upstream methodology and the Normative Draft. These follow upstream dev, which may be newer than this snapshot. The judge is under development: current declared-template findings are Observe warnings, not admission blockers; other checks have independent effects. The draft describes the wider design, not a completed judge. A rule’s module delta selection decides what to inspect; it is separate from removing an entry from one fixed catalog above.

Try your own question: find a pair of states your observations cannot distinguish. Name the state space, the observations, an added readout and any ambiguity that remains. Follow the current journey and repository skills guidance to explore the definitions and develop a contribution with Claude Code or Codex.