VacuityFloors

How much searching a binding's generator has to do before its green counts for anything.

A lattice law is a statement about a set of states, so a green run says exactly as much as the pool it ran over. LatticeLawHarness measures four rates while it builds that pool and fails the binding when one falls outside these bounds — not because the type is broken, but because the evidence is too thin to say it is not. The measured values print on a green run too (LatticeLawHarness.measureVacuity), because a floor whose actual value nobody sees is a floor nobody notices drifting toward.

The pair definition, stated exactly

This is the one thing about these floors that must not be left to the reader, and it has already been read two ways: two independent measurements of ORSetConvergenceTest reported 66.7% and 30.4% strict ancestry over the same pool builder — a factor of 2.2, entirely definitional.

A "pair" is an ordered pair of distinct pool positions. For a pool of n states the denominator is n(n − 1) — (i, j) and (j, i) are two pairs, and (i, i) is not a pair. Both numerators are then counted over that same denominator:

• strict-ancestor counts (a, b) with a ⊔ b == b and b ⊔ a != a — a is strictly below b. Only one of the two directions of a comparable pair ever counts, so a total order reads 50%, not 100% — that is the ceiling, and IntMax's chain sits exactly on it.

• concurrent counts (a, b) with a ⊔ b != b and b ⊔ a != a — neither is below the other. Incomparability is symmetric, so both directions count.

The two are therefore related by 2 × strictAncestor + concurrent + equal = 100%, where equal is the pairs of positions holding the same value (a no-op step puts one in the pool). That identity is worth checking against any number quoted here: the design's controlled experiment reads 2 × 30.15 + 39.69 = 99.99, which is what makes its convention recoverable at all.

The alternative reading — count unordered pairs {a, b} in which either is a strict ancestor, over n(n − 1)/2 — is not wrong, it is just twice as large, and it loses the 50% chain ceiling that makes a total order legible at a glance. Everything here uses the ordered one.

The step rates

A step is one op the pool builder applied to a replica: every op of every critical shape, plus every op of the random exploration. Absorbing a peer's state (the gossip draw) is not a step — it is not drawn from the alphabet and has no OpKind to classify.

Whether the critical-shape ops count is a real choice, and it moves the numbers a long way. ORSetConvergenceTest reads 20.3% no-ops counting them and 27.9% excluding them, on the same pool over the same seeds — one side of a 25% ceiling to the other. The case for excluding them is that the harness already asserts every shape step changed the state, so they are validated constants that dilute a ceiling and inflate a floor. They are counted anyway, for three reasons:

1. They are not free. A shape whose step does not move the state fails the binding outright, so a shape cannot be padding — declaring one is doing the work, not dodging it.

2. They are the design's own thesis. Constructed shapes are what reach the interesting configuration on every seed rather than on a lucky one. A denominator that excludes exactly the constructed part measures only the part this suite considers weaker.

3. Consistency with the pair rates. Ancestry and concurrency are measured over the whole pool, shape states included. Excluding shape steps would have one table describing two different populations.

The cost is that the default assert · retire · assert shape contributes about 9 points of retirement rate at these pool sizes — most of the 10% floor — so a binding must not be read as clearing the retirement floor on its shape alone. Every retiring binding in the tree clears it with room to spare on exploration too (the lowest is 19.8%), and a binding that sat near 10% would be worth looking at rather than passing.

• effective retire steps — steps whose op is OpKind.RETIRE and which changed the state. The and is the whole point: a remove of something absent is the lattice identity, and a generator can spend most of its budget there. This is the floor the design exists for; see OpKind for the controlled experiment showing it is the only one of the four that separates a searching generator from a vacuous one.

• no-op steps — steps of any kind that left the state unchanged. A ceiling, not a floor.

The two waivers, and why they are shaped differently

totalOrder is a boolean, because "this pool is a chain" is a structural claim about the type — IntMax cannot be given concurrency by a better generator, and pretending otherwise would mean fabricating states it cannot reach. It waives the concurrency floor only; a total order still has to clear ancestry (it reads 50%), retirement and no-ops.

Having nothing to retire gets no boolean. Such a binding sets effectiveRetireSteps = 0.0 and says why in a comment — see NOTHING_TO_RETIRE. The asymmetry is deliberate: a growOnly = true flag would be reachable by deleting a binding's retiring op, and deleting the retiring op is exactly the mutation this floor exists to catch. Spelling the waived value out keeps the floor at its default on every binding that has something to retire, so removing that op reds it rather than quietly reclassifying it.

Parameters