runExhaustiveSmall

Both bracketing laws over every word of length 1..L the alphabet can spell, on one replica — and on failure, the shortest word that breaks them. Returns the number of words searched on a green run.

This is the shrinking replacement, and it is a better artefact than a shrinker's. Words are enumerated breadth-first by length, so the first one that fails is the shortest one that can: every shorter word was already tried and passed. A property-based shrinker reports a locally minimal synthetic operand list — three states it narrowed by re-running a generator; this reports the globally shortest reachable trajectory, named in the binding's own vocabulary, with the exact prefixes that produced a, b and c. Re-running the reported word from initial reproduces it exactly, because each word gets a fresh Random seeded identically, so a word — not a seed plus a trial number — is the whole repro.

Measured against a lattice that wrongly keeps a retired contribution (the pre-#2099 ORMap), this pass reports [put-high, remove, put-low] — length 3, the shape #2086 needs. How many words it took to get there is a property of the alphabet, not of the search: 28 over [put-low, put-high, remove], 20 over [put-high, put-low, remove], 47 over the five ops ORMapConvergenceTest actually declares. The length is the claim; the count is bookkeeping.

One replica, so the pool is a chain, and that is the point. The randomised pass explores width: three replicas, gossip, POOL_LIMIT states, sixteen seeds. This explores depth exhaustively at tiny sizes, where "exhaustively" is what buys the minimality claim. A chain is not a weaker pool than a forked one for this purpose — a broken join is exactly one that fails to be a join, and a chain i ≤ s₁ ≤ … ≤ sₙ is where that shows most legibly, because a correct lattice makes every join on it trivially the later operand.

The bound is EXHAUSTIVE_WORD_LENGTH, capped by EXHAUSTIVE_TRIPLE_BUDGET — read both before changing either.