An expansion atom's pack

An expansion atom runs the same machinery a gate does, one exponent along: it reads the tags of its argument points, branches on the tuple they decode, and folds the defining sentence of that branch. So every piece it needs is one already discharged for the gates, at the branch's prefix rather than the domain's – the naming guards through DescriptiveComplexity.Draw.Data.encCoord, the leaf from the control, and the three shapes of a fold.

With them, DescriptiveComplexity.Draw.UTagArgsDef of DescriptiveComplexity.Draw.Data.expArgs is a field-by-field check.

What a branch reads

A branch's three folds

The pack

A comparison's pack

The equality and order atoms of a matrix compare two points, and the machine does it by walking their two registers in step. What it keeps between rounds is three scratch flags – agreement so far, a difference seen, and its direction – so its folds are nested single-slot writes over the narrow loop element.

A stage atom's pack

A gate block's pack

An atom's pack, by kind

The whole pack of a variable

theorem DescriptiveComplexity.Draw.Data.uVarArgsDef_varArgsOf {L : FirstOrder.Language} [L.IsRelational] {dt : Data L} [Fintype dt.SlotIx] (e₀ : Env L) (v : dt.VarIx) : UVarArgsDef v fun (e : Env L) => dt.varArgsOf e.zero e.one v

The semantic pack of one variable's machinery meets its obligation. This is the last thing the program's rules owe the interpretation: with it, DescriptiveComplexity.Draw.Data.uRulesDefinable_progAsm applies to the reduction's own machine.

theorem DescriptiveComplexity.Draw.Data.uRulesDefinable_progOf {L : FirstOrder.Language} [L.IsRelational] {dt : Data L} [Fintype dt.SlotIx] (e₀ : Env L) : URulesDefinable fun (e : Env L) => dt.outerRule e.zero e.one (dt.evalRuleF e.zero e.one fun (v : dt.VarIx) => dt.varArgsOf e.zero e.one v) (EvalPh.chk 0) (EvalPh.sub dt.smEntryOut)

The EXPSPACE program's whole rule set is definable. Every rule of the reduction's own machine – its guard, the pointer it leaves and the tracks it writes – is written down by one formula for every instance, so the eleven relations of FirstOrder.Language.wide can be emitted by an interpretation. The one environment it asks for is what names the dispatch's default tag.