research

Most accounts of distinction begin with a single agent drawing a line. We argue that this gets the order wrong. Distinction is not a one-body achievement but a coordination problem: it emerges when two systems under shared pressure make one's differentiation legible to the other. The first distinction is not made but recognized. This has consequences for how we think about the origin of symbolic structure — and for what counts as a genuine category versus a convenient partition.

A cut is a distinction's relation to the field it partitions. A fold is a distinction's relation to other distinctions — specifically, inclusion. These are not operations applied to an inert substrate; they are structural aspects of every distinction. Organized clusters of folds constitute policies — coherent configurations that can stabilize or fail to stabilize under pressure. Much of the lab's formal work concerns what policies do once applied and under what conditions they achieve coherence.

Every distinction excludes. What it excludes — the remainder — does not disappear but persists as pressure on the system that produced it. In reflexive social contexts this pressure becomes strategic: the 49.9 million “Some Other Race” responses in the 2020 US Census are remainder produced by a classification scheme, not noise. Opacity is the gradient of access to the structure behind a distinction — relational, not intrinsic. The same category can be transparent to those who administer it and opaque to those who live under it. These phenomena are studied across social science, aesthetics, and AI.

Spencer-Brown begins: “Draw a distinction.” But if no distinction is yet present, there is no drawer, no instrument, no field. The capacity to draw presupposes that agent and surface are already differentiated. Some distinctions are drawn — imposed by the apparatus of the symbolic world and held in place by constraint. Others emerge endogenously, tracking features of the world that are invariant under perturbation. The relationship between these two sources is complicated by the fact that constraint can produce fit: the world reshapes itself around imposed categories until they begin to look natural.

The lab maintains a formal backbone in Agda — a dependently typed proof assistant that guarantees every accepted proof is valid. All proofs compile under --safe --without-K: no postulates, no escape hatches. The current codebase spans 174 modules and over 34,000 lines of verified code. Agda proves what we ask it to prove, and coherence is not correctness — the gap between formalization and theory is tracked explicitly. Claims that can be checked are claims that can travel.