The matrix and the gates carry definability #
One variable's machinery is a matrix – the sequencer over the classified atoms of its step formula – and two runs of gates – sequencers over the argument blocks and over the quantified levels, each block a well-shapedness file test followed by a tag-branched domain evaluation. All four are sequencers over things already discharged, so all four are one line plus the checkpoints' control updates.
The only new shape is a gate block's verdict exit, whose destination
pointer branches on a bit that the kit fixes, not the data: passing leaves
the pointer alone, failing applies the caller's clearing update, and
DescriptiveComplexity.Draw.UStDefinable.ite decides which when the formula is
built.