A gate's four folds #
What a gate block's element loop carries between rounds is a composite write: started, it clears the loop element and sets the sub-fold to its polarity's unit; advanced, it stores the leaf, folds at the carry coordinate and steps the loop element; and its exit conjoins the sub-fold's verdict into the block's flag.
Each is two or three writes nested, and what makes them definable is not new machinery but the commutations: the three registers a gate writes – the loop element, the sub-fold's accumulators, and the sub-leaf flag – are disjoint, so each write reads what it was given. With those, the pieces are the ones already discharged.
The three registers are disjoint #
Composing a write with a write #
The three shapes a fold has #
A gate block and an expansion atom fold the same way – only the prefix and the leaf differ – so the three shapes are stated at an arbitrary polarity and an arbitrary definable leaf, and each machinery instantiates them.