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.

The matrix

theorem DescriptiveComplexity.Draw.Data.uRulesDefinable_matrixRule {L : FirstOrder.Language} {dt : Data L} {Q P : Type} [Fintype Q] [Fintype dt.SlotIx] {v : dt.VarIx} {emb : dt.MatrixPh v → P} {argsA : (e : Env L) → (a : Fin (dt.natOf v)) → dt.KindArgs (dt.kindOf v a)} {enterSt : (e : Env L) → Fin (dt.natOf v) → (Q → e.α) → (dt.SlotIx → e.α) → Q → e.α} {exitPh : P} (hA : ∀ (a : Fin (dt.natOf v)), UKindArgsDef (dt.kindOf v a) fun (e : Env L) => argsA e a) (hen : ∀ (a : Fin (dt.natOf v)), UStDefinable fun (e : Env L) => enterSt e a) : URulesDefinable fun (e : Env L) => dt.matrixRule e.zero e.one v emb (argsA e) (enterSt e) exitPh

A matrix's rules are definable: the sequencer over the classified atoms, each stage its kind's machinery.

One gate block

theorem DescriptiveComplexity.Draw.Data.uRulesDefinable_gateBlockRule {L : FirstOrder.Language} {dt : Data L} {Q P : Type} [Fintype Q] [Fintype dt.SlotIx] {emb : dt.GateBlockPh → P} {args : (e : Env L) → TagArgs e.α Q dt.SlotIx (Fintype.card dt.X.Tag) dt.X.Tag dt.domNr} {wellG : (e : Env L) → (dt.SlotIx → e.α) → Prop} {setFail : (e : Env L) → (Q → e.α) → (dt.SlotIx → e.α) → Q → e.α} {failPh exitPh : P} (hwell : UGDefinable fun (e : Env L) (x : Q → e.α) (g : dt.SlotIx → e.α) => wellG e g) (hfail : UStDefinable setFail) (hargs : UTagArgsDef args) : URulesDefinable fun (e : Env L) => dt.gateBlockRule e.one emb (args e) (wellG e) (setFail e) failPh exitPh

A gate block's rules are definable: the well-shapedness file test, its two verdict exits – the failing one clearing the caller's flag – and the tag-branched domain evaluation.

The two runs of gates

theorem DescriptiveComplexity.Draw.Data.uRulesDefinable_gatesRule {L : FirstOrder.Language} {dt : Data L} {Q P : Type} [Fintype Q] [Fintype dt.SlotIx] {v : dt.VarIx} {emb : dt.GatesPh v → P} {argsG : (e : Env L) → Fin (dt.arOf v) → TagArgs e.α Q dt.SlotIx (Fintype.card dt.X.Tag) dt.X.Tag dt.domNr} {wellGOf : (e : Env L) → Fin (dt.arOf v) → (dt.SlotIx → e.α) → Prop} {setFail : (e : Env L) → (Q → e.α) → (dt.SlotIx → e.α) → Q → e.α} {enterSt : (e : Env L) → Fin (dt.arOf v) → (Q → e.α) → (dt.SlotIx → e.α) → Q → e.α} {failPh exitPh : P} (hwell : ∀ (b : Fin (dt.arOf v)), UGDefinable fun (e : Env L) (x : Q → e.α) (g : dt.SlotIx → e.α) => wellGOf e b g) (hfail : UStDefinable setFail) (hargs : ∀ (b : Fin (dt.arOf v)), UTagArgsDef fun (e : Env L) => argsG e b) (hen : ∀ (b : Fin (dt.arOf v)), UStDefinable fun (e : Env L) => enterSt e b) : URulesDefinable fun (e : Env L) => dt.gatesRule e.one v emb (argsG e) (wellGOf e) (setFail e) (enterSt e) failPh exitPh

The gates' rules are definable: the sequencer over the argument blocks.

theorem DescriptiveComplexity.Draw.Data.uRulesDefinable_igatesRule {L : FirstOrder.Language} {dt : Data L} {Q P : Type} [Fintype Q] [Fintype dt.SlotIx] {v : dt.VarIx} {emb : dt.IGatesPh v → P} {argsG : (e : Env L) → Fin (dt.nIn v) → TagArgs e.α Q dt.SlotIx (Fintype.card dt.X.Tag) dt.X.Tag dt.domNr} {wellGOf : (e : Env L) → Fin (dt.nIn v) → (dt.SlotIx → e.α) → Prop} {setFailOf enterSt : (e : Env L) → Fin (dt.nIn v) → (Q → e.α) → (dt.SlotIx → e.α) → Q → e.α} {exitPh : P} (hwell : ∀ (b : Fin (dt.nIn v)), UGDefinable fun (e : Env L) (x : Q → e.α) (g : dt.SlotIx → e.α) => wellGOf e b g) (hfail : ∀ (b : Fin (dt.nIn v)), UStDefinable fun (e : Env L) => setFailOf e b) (hargs : ∀ (b : Fin (dt.nIn v)), UTagArgsDef fun (e : Env L) => argsG e b) (hen : ∀ (b : Fin (dt.nIn v)), UStDefinable fun (e : Env L) => enterSt e b) : URulesDefinable fun (e : Env L) => dt.igatesRule e.one v emb (argsG e) (wellGOf e) (setFailOf e) (enterSt e) exitPh

The inner gates' rules are definable: the same sequencer, every fail exit continuing to the next block with the level's flag cleared.