The folds are definable #
What the program's control holds between rounds is a fold: one accumulator
per level of a quantifier prefix, closed by a leaf flag. Reading it back is
DescriptiveComplexity.Draw.chainFrom, a recursion down the levels, and writing
it at a carry is DescriptiveComplexity.Draw.Data.putVec of a family whose
entries branch on the carry.
Both are definable, and for the same reason: the recursion is over a fixed
number of levels, so recursing the same way builds the pattern function. The
atoms are DescriptiveComplexity.Draw.Data.uGDefinable_readVec and
uGDefinable_ctlBit; everything else is the connectives.
The matrix's own value at the atoms' verdicts
(DescriptiveComplexity.Draw.qfValue) is the same shape one level down – a
recursion over the syntax rather than over the levels – so it is here too.