The matrix's and the gates' rules

One layer up from the kind dispatch: the matrix of a variable is the sequencer over its classified atoms – each stage the kind's machinery, its exit the next checkpoint – and the gates are the sequencer over the argument blocks, each block a well-shapedness file test whose passing exit enters the tag-branched domain evaluation and whose failing exit leaves the whole gate sequence with the verdict flag cleared.

As below, the semantic parameters ride in packs and dstSt parameters; the shapes and separations close here.

The matrix

noncomputable def DescriptiveComplexity.Draw.Data.matrixRule {L : FirstOrder.Language} (dt : Data L) {A Q P : Type} (zero one : A) (v : dt.VarIx) (emb : dt.MatrixPh v → P) (argsA : (a : Fin (dt.natOf v)) → dt.KindArgs (dt.kindOf v a)) (enterSt : Fin (dt.natOf v) → (Q → A) → (dt.SlotIx → A) → Q → A) (exitPh : P) (i : dt.MatrixSite v) : dt.MatrixSh v i → Rule A Q dt.SlotIx P

The matrix's rules: the sequencer over the classified atoms, each stage its kind's machinery, its exit the next checkpoint.

Equations

• One or more equations did not get rendered due to their size.

One gate block

noncomputable def DescriptiveComplexity.Draw.Data.gateDomEntry {L : FirstOrder.Language} (dt : Data L) {P : Type} (emb : dt.GateBlockPh → P) : P

The entry of the domain evaluation.

Equations

• dt.gateDomEntry emb = DescriptiveComplexity.Draw.tagFirstRd fun (p : DescriptiveComplexity.Draw.TagPh (Fintype.card dt.X.Tag) dt.X.Tag dt.domNr) => emb (Sum.inr p)

noncomputable def DescriptiveComplexity.Draw.Data.gateBlockRule {L : FirstOrder.Language} (dt : Data L) {A Q P : Type} (one : A) (emb : dt.GateBlockPh → P) (args : TagArgs A Q dt.SlotIx (Fintype.card dt.X.Tag) dt.X.Tag dt.domNr) (wellG : (dt.SlotIx → A) → Prop) (setFail : (Q → A) → (dt.SlotIx → A) → Q → A) (failPh exitPh : P) (i : dt.GateBlockSite) : dt.GateBlockSh i → Rule A Q dt.SlotIx P

One gate block's rules: the well-shapedness file test – its passing exit entering the domain evaluation, its failing exit leaving the whole gate sequence with the verdict flag cleared – and the tag-branched domain evaluation.

Equations

• One or more equations did not get rendered due to their size.

The gates

noncomputable def DescriptiveComplexity.Draw.Data.gatesRule {L : FirstOrder.Language} (dt : Data L) {A Q P : Type} (one : A) (v : dt.VarIx) (emb : dt.GatesPh v → P) (argsG : Fin (dt.arOf v) → TagArgs A Q dt.SlotIx (Fintype.card dt.X.Tag) dt.X.Tag dt.domNr) (wellGOf : Fin (dt.arOf v) → (dt.SlotIx → A) → Prop) (setFail : (Q → A) → (dt.SlotIx → A) → Q → A) (enterSt : Fin (dt.arOf v) → (Q → A) → (dt.SlotIx → A) → Q → A) (failPh exitPh : P) (i : dt.GatesSite v) : dt.GatesSh v i → Rule A Q dt.SlotIx P

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

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.Draw.Data.gatesHosrc {L : FirstOrder.Language} (dt : Data L) {A Q P : Type} (one : A) (v : dt.VarIx) {emb : dt.GatesPh v → P} (argsG : Fin (dt.arOf v) → TagArgs A Q dt.SlotIx (Fintype.card dt.X.Tag) dt.X.Tag dt.domNr) (wellGOf : Fin (dt.arOf v) → (dt.SlotIx → A) → Prop) (setFail : (Q → A) → (dt.SlotIx → A) → Q → A) (enterSt : Fin (dt.arOf v) → (Q → A) → (dt.SlotIx → A) → Q → A) (failPh exitPh : P) (i : dt.GatesSite v) (ρ : dt.GatesSh v i) : ∃ (p : dt.GatesPh v), (dt.gatesRule one v emb argsG wellGOf setFail enterSt failPh exitPh i ρ).srcPh = emb p ∧ seqOwn (fun (x : Fin (dt.arOf v)) => dt.gateBlockOwn) p = i

Every rule of the gates fires from a phase its site owns.

The inner gates

The same sequencer-over-gate-blocks as the outer gates, with one difference: a failing block does not abort the sequence – every quantified level's flag must be computed, since the leaf reads both flag conjunctions whichever way the branch goes. So each block's fail exit continues to the next checkpoint, its setFail clearing the level's polarity flag.

noncomputable def DescriptiveComplexity.Draw.Data.igatesRule {L : FirstOrder.Language} (dt : Data L) {A Q P : Type} (one : A) (v : dt.VarIx) (emb : dt.IGatesPh v → P) (argsG : Fin (dt.nIn v) → TagArgs A Q dt.SlotIx (Fintype.card dt.X.Tag) dt.X.Tag dt.domNr) (wellGOf : Fin (dt.nIn v) → (dt.SlotIx → A) → Prop) (setFailOf enterSt : Fin (dt.nIn v) → (Q → A) → (dt.SlotIx → A) → Q → A) (exitPh : P) (i : dt.IGatesSite v) : dt.IGatesSh v i → Rule A Q dt.SlotIx P

The inner gates' rules: the sequencer over the quantified levels' blocks, every fail exit continuing.

Equations

• One or more equations did not get rendered due to their size.