To XOR a Stone with Six Birds: Closure Diagnostics for Emergent Bits, Gates, and Booleanity

When does a physical or stochastic system deserve to be described in terms of bits and logic gates? We treat logic not as a starting point but as something a coarse-grained description has to earn. Working in the Six Birds emergence calculus, we call a description a logic layer when it is an audited closure of packaged predicates under induced dynamics: its binary labels persist, the underlying dynamics descends to update rules on those labels, and what the description gets wrong or leaves out is measured explicitly. We turn this definition into a set of diagnostics (predicate stability, route mismatch, closure defect, channel error and entropy, unretained input information, and entropy-production audits) and apply them to finite Markov laboratories in which NOT, AND, and reversible XOR (CNOT) gates run under controlled noise, metastability, and coarse-graining. Four results follow. First, in a laboratory with leaky parity sectors, the parity bit is an exactly closed coarse variable, with route mismatch zero at every leakage rate and horizon, whereas the other balanced binary partitions and the AND predicate have strictly positive mismatch at every tested leakage rate and horizon; closed-form expressions give the size of the gap. Second, the three gates fail in different ways: NOT and AND lose closure when their stored inputs drift, whereas a noiseless one-step CNOT is a perfect input–output channel even though its output bit, read alone, is maximally unclosed. Third, reading the same CNOT laboratory through its XOR output instead of its full register raises the input information left unaccounted for by the output from h2(0.02) ≈ 0.141 bits to 1 + h2(0.02) bits, a factor of 8.07 that rational bounds certify to exceed eight, and raises route mismatch from 0 to 0.96. Fourth, a simple unsupervised pipeline recovers the intended stable bits from transition structure alone and reconstructs a NOT gate in declared label coordinates. The predicate and quotient facts on which the framework rests are formalized in Lean 4, and the main experimental quantities are re-derived independently in closed form, with their probabilities and route mismatches checked in exact rational arithmetic. The result is a falsifiable, layer-relative criterion for when a system has logic, and for which logic it has. Code, data, and the Lean formalization: https://github.com/ioannist/six-birds-logic