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

theorem DescriptiveComplexity.Draw.Data.uGDefinable_tagMatch {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] (v : dt.VarIx) {k : ℕ} (ts : Fin k → Fin (dt.nOf v)) (ℓ : Fin k) (t : dt.X.Tag) : UGDefinable fun (e : Env L) (f : dt.CtlIx → e.α) (g : dt.SlotIx → e.α) => dt.tagMatch e.zero e.one v ts ℓ t f g

A witness read's name is definable: the tag's encoded tuple in the block of the level the position reads.

theorem DescriptiveComplexity.Draw.Data.uGDefinable_TagsAre {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] {k : ℕ} (hk : k * Fintype.card dt.X.Tag ≤ dt.ntgDim) (τ : Fin k → dt.X.Tag) : UGDefinable fun (e : Env L) (f : dt.CtlIx → e.α) (x : dt.SlotIx → e.α) => dt.TagsAre e.one hk τ f

A branch's decoding is definable: one-hotness of the witness flags, at every argument position.

theorem DescriptiveComplexity.Draw.Data.uGDefinable_expMatch {L : FirstOrder.Language} [L.IsRelational] {dt : Data L} [Fintype dt.SlotIx] (v : dt.VarIx) {k : ℕ} (ts : Fin k → Fin (dt.nOf v)) (e' : dt.X.E.Relations k) (τ : Fin k → dt.X.Tag) (r : Fin (dt.relNr e' τ)) (hn : (dt.relPk e' τ).n ≤ dt.eDim) : UGDefinable fun (e : Env L) (f : dt.CtlIx → e.α) (g : dt.SlotIx → e.α) => dt.expMatch e.zero e.one v ts e' τ r hn f g

A read leaf's name is definable: the member tuple of the copy's point, its payload the loop element at the levels the leaf's atom reads.

theorem DescriptiveComplexity.Draw.Data.uGDefinable_expLeafVal {L : FirstOrder.Language} [L.IsRelational] {dt : Data L} [Fintype dt.SlotIx] {k : ℕ} (e' : dt.X.E.Relations k) (τ : Fin k → dt.X.Tag) (hn : (dt.relPk e' τ).n ≤ dt.eDim) (hrd : dt.relNr e' τ ≤ dt.nfDim) : UGDefinable fun (e : Env L) (f : dt.CtlIx → e.α) (x : dt.SlotIx → e.α) => dt.expLeafVal e.one e' τ hn hrd f

The value of a branch's matrix from the control is definable, exactly as a domain sentence's is.

A branch's three folds

theorem DescriptiveComplexity.Draw.Data.uStDefinable_expInit {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] {k : ℕ} (e' : dt.X.E.Relations k) (τ : Fin k → dt.X.Tag) : UStDefinable fun (e : Env L) (f : dt.CtlIx → e.α) (x : dt.SlotIx → e.α) => dt.expInit e.zero e.one e' τ f

A branch's loop, started.

theorem DescriptiveComplexity.Draw.Data.uStDefinable_expAdv {L : FirstOrder.Language} [L.IsRelational] {dt : Data L} [Fintype dt.SlotIx] {k : ℕ} (e' : dt.X.E.Relations k) (τ : Fin k → dt.X.Tag) (hn : (dt.relPk e' τ).n ≤ dt.eDim) (hrd : dt.relNr e' τ ≤ dt.nfDim) : UStDefinable fun (e : Env L) (f : dt.CtlIx → e.α) (x : dt.SlotIx → e.α) => dt.expAdv e.zero e.one e' τ hn hrd f

A branch's round, folded and advanced.

theorem DescriptiveComplexity.Draw.Data.uStDefinable_expExit {L : FirstOrder.Language} [L.IsRelational] {dt : Data L} [Fintype dt.SlotIx] {k : ℕ} (e' : dt.X.E.Relations k) (τ : Fin k → dt.X.Tag) (hn : (dt.relPk e' τ).n ≤ dt.eDim) (hrd : dt.relNr e' τ ≤ dt.nfDim) (a : Fin dt.natMax) : UStDefinable fun (e : Env L) (f : dt.CtlIx → e.α) (x : dt.SlotIx → e.α) => dt.expExit e.zero e.one e' τ hn hrd a f

A branch's last round: the final leaf filed and the sub-fold's verdict into the atom's slot.

The pack

theorem DescriptiveComplexity.Draw.Data.uTagArgsDef_expArgs {L : FirstOrder.Language} [L.IsRelational] {dt : Data L} [Fintype dt.SlotIx] {k : ℕ} (v : dt.VarIx) (ts : Fin k → Fin (dt.nOf v)) (e' : dt.X.E.Relations k) (a : Fin dt.natMax) (hk : k * Fintype.card dt.X.Tag ≤ dt.ntgDim) (hn : ∀ (τ : Fin k → dt.X.Tag), (dt.relPk e' τ).n ≤ dt.eDim) (hrd : ∀ (τ : Fin k → dt.X.Tag), dt.relNr e' τ ≤ dt.nfDim) : UTagArgsDef fun (e : Env L) => dt.expArgs e.zero e.one v ts e' a hk hn hrd

An expansion atom's pack meets its obligation, field by field.

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.

theorem DescriptiveComplexity.Draw.Data.uStDefinable_putLv_comp {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] {w : (e : Env L) → (dt.CtlIx → e.α) → (dt.SlotIx → e.α) → Fin dt.dd0 → e.α} (hw : ∀ (j : Fin dt.dd0), USlotDefinable fun (e : Env L) (f : dt.CtlIx → e.α) (g : dt.SlotIx → e.α) => w e f g j) {F : (e : Env L) → (dt.CtlIx → e.α) → (dt.SlotIx → e.α) → dt.CtlIx → e.α} (hF : UStDefinable F) : UStDefinable fun (e : Env L) (f : dt.CtlIx → e.α) (g : dt.SlotIx → e.α) => dt.putLv (F e f g) (w e f g)

A narrow loop-element write over a definable base.

theorem DescriptiveComplexity.Draw.Data.uStDefinable_cmpFold {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] (hnf : 2 ≤ dt.nfDim) : UStDefinable fun (e : Env L) (f : dt.CtlIx → e.α) (x : dt.SlotIx → e.α) => dt.cmpFold e.zero e.one hnf f

A comparison's bookkeeping, folded: three scratch flags, each written from a question about the round's two reads.

theorem DescriptiveComplexity.Draw.Data.uStDefinable_cmpInit_initLvN {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] : UStDefinable fun (e : Env L) (f : dt.CtlIx → e.α) (x : dt.SlotIx → e.α) => dt.cmpInit e.zero e.one (dt.initLvN f)

A comparison's bookkeeping, started.

theorem DescriptiveComplexity.Draw.Data.uGDefinable_cmpVerdict_cmpFold {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] (hnf : 2 ≤ dt.nfDim) (isEq : Bool) : UGDefinable fun (e : Env L) (f : dt.CtlIx → e.α) (x : dt.SlotIx → e.α) => dt.cmpVerdict e.one isEq (dt.cmpFold e.zero e.one hnf f)

A comparison's verdict, read off the folded flags.

theorem DescriptiveComplexity.Draw.Data.uElemArgsDef_cmpArgs {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] (v : dt.VarIx) (a : Fin dt.natMax) (hnf : 2 ≤ dt.nfDim) (isEq : Bool) (j₁ j₂ : Fin (dt.nOf v)) : UElemArgsDef fun (e : Env L) => dt.cmpArgs e.zero e.one v a hnf isEq j₁ j₂

A comparison's pack meets its obligation.

A stage atom's pack

theorem DescriptiveComplexity.Draw.Data.uStageArgsDef_stageArgs {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] (v : dt.VarIx) (i : dt.d.B.ι) (ts : Fin (dt.d.B.arity i) → Fin (dt.nOf v)) (a : Fin dt.natMax) : UStageArgsDef fun (e : Env L) => dt.stageArgs e.zero e.one v i ts a

A stage atom's pack meets its obligation: everything it names is static, and the two bits it writes are flags.

A gate block's pack

theorem DescriptiveComplexity.Draw.Data.uTagArgsDef_gateArgs {L : FirstOrder.Language} [L.IsRelational] {dt : Data L} [Fintype dt.SlotIx] (e₀ : Env L) (b : Fin dt.ko ⊕ Fin dt.ki) (hc : Fintype.card dt.X.Tag ≤ dt.ntgDim) (hn : ∀ (t : dt.X.Tag), (dt.domPk t).n ≤ dt.eDim) (hrd : ∀ (t : dt.X.Tag), dt.domNr t ≤ dt.nfDim) : UTagArgsDef fun (e : Env L) => dt.gateArgs e.zero e.one b hc hn hrd

A gate block's pack meets its obligation: the witness reads are named by the tags' encoded tuples, the leaf reads by the members of the gated point, and the three folds are the gate's. The one thing that needs an environment is the default branch of the dispatch, which names a tag.

theorem DescriptiveComplexity.Draw.Data.uTagArgsDef_igateArgs {L : FirstOrder.Language} [L.IsRelational] {dt : Data L} [Fintype dt.SlotIx] (e₀ : Env L) (b : Fin dt.ko ⊕ Fin dt.ki) (flag : dt.CtlIx) (hc : Fintype.card dt.X.Tag ≤ dt.ntgDim) (hn : ∀ (t : dt.X.Tag), (dt.domPk t).n ≤ dt.eDim) (hrd : ∀ (t : dt.X.Tag), dt.domNr t ≤ dt.nfDim) : UTagArgsDef fun (e : Env L) => dt.igateArgs e.zero e.one b flag hc hn hrd

An inner gate block's pack, the same with the reads on VAL and the verdict into the level's flag.

An atom's pack, by kind

theorem DescriptiveComplexity.Draw.Data.uKindArgsDef_kindArgsOf {L : FirstOrder.Language} [L.IsRelational] {dt : Data L} [Fintype dt.SlotIx] (v : dt.VarIx) (a : Fin dt.natMax) (κ : MatAtom dt.X dt.d.B (dt.nOf v)) (hk : dt.kindArgs κ * Fintype.card dt.X.Tag ≤ dt.ntgDim) (hn : dt.kindDepth κ ≤ dt.eDim) (hrd : dt.kindReads κ ≤ dt.nfDim) : UKindArgsDef κ fun (e : Env L) => dt.kindArgsOf e.zero e.one v a κ hk hn hrd

Every atom kind's pack meets its obligation, one constructor at a time.

theorem DescriptiveComplexity.Draw.Data.uKindArgsDef_atomArgs {L : FirstOrder.Language} [L.IsRelational] {dt : Data L} [Fintype dt.SlotIx] (v : dt.VarIx) (a : Fin (dt.natOf v)) : UKindArgsDef (dt.kindOf v a) fun (e : Env L) => dt.atomArgs e.zero e.one v a

The pack of the a-th atom of a variable's matrix.

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.