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.

theorem DescriptiveComplexity.Draw.Data.matrixHosrc {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) : ∃ (p : dt.MatrixPh v), (dt.matrixRule zero one v emb argsA enterSt exitPh i ρ).srcPh = emb p ∧ seqOwn (fun (a : Fin (dt.natOf v)) => dt.kindOwn (dt.kindOf v a)) p = i

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

theorem DescriptiveComplexity.Draw.Data.matrixRule_dstIn {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) {S : P → Prop} (hemb : ∀ (p : dt.MatrixPh v), S (emb p)) (hexit : S exitPh) (i : dt.MatrixSite v) (ρ : dt.MatrixSh v i) : S (dt.matrixRule zero one v emb argsA enterSt exitPh i ρ).dstPh

A property of the matrix's phases and its exit holds of every phase it can move to: each atom's machinery stays inside its own and its verdict goes to the next checkpoint.

theorem DescriptiveComplexity.Draw.Data.matrixSep {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) (hzo : zero ≠ one) (hemb : Function.Injective emb) (i : dt.MatrixSite v) (ρ ρ' : dt.MatrixSh v i) (f : Q → A) (g : dt.SlotIx → A) : (dt.matrixRule zero one v emb argsA enterSt exitPh i ρ).guard f g → (dt.matrixRule zero one v emb argsA enterSt exitPh i ρ').guard f g → (dt.matrixRule zero one v emb argsA enterSt exitPh i ρ).srcPh = (dt.matrixRule zero one v emb argsA enterSt exitPh i ρ').srcPh → ρ = ρ'

The matrix separates in-shape.

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.

theorem DescriptiveComplexity.Draw.Data.gateBlockRule_dstPh {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) : (∃ (p : dt.GateBlockPh), (dt.gateBlockRule one emb args wellG setFail failPh exitPh i ρ).dstPh = emb p) ∨ (dt.gateBlockRule one emb args wellG setFail failPh exitPh i ρ).dstPh = failPh ∨ (dt.gateBlockRule one emb args wellG setFail failPh exitPh i ρ).dstPh = exitPh

A gate block leaves only into its own phases, its failing exit or its exit: the file test's trip stays inside it, its passing exit enters the domain evaluation, and the tag machinery's rules leave only where it leaves.

theorem DescriptiveComplexity.Draw.Data.gateBlockRule_dstIn {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) {S : P → Prop} (hemb : ∀ (p : dt.GateBlockPh), S (emb p)) (hfail : S failPh) (hexit : S exitPh) (i : dt.GateBlockSite) (ρ : dt.GateBlockSh i) : S (dt.gateBlockRule one emb args wellG setFail failPh exitPh i ρ).dstPh

A property of a gate block's phases, its failing exit and its exit holds of every phase it can move to.

theorem DescriptiveComplexity.Draw.Data.gateBlockHosrc {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) : ∃ (p : dt.GateBlockPh), (dt.gateBlockRule one emb args wellG setFail failPh exitPh i ρ).srcPh = emb p ∧ dt.gateBlockOwn p = i

Every rule of a gate block fires from a phase its site owns.

theorem DescriptiveComplexity.Draw.Data.gateBlockSep {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) (hemb : Function.Injective emb) (i : dt.GateBlockSite) (ρ ρ' : dt.GateBlockSh i) (f : Q → A) (g : dt.SlotIx → A) : (dt.gateBlockRule one emb args wellG setFail failPh exitPh i ρ).guard f g → (dt.gateBlockRule one emb args wellG setFail failPh exitPh i ρ').guard f g → (dt.gateBlockRule one emb args wellG setFail failPh exitPh i ρ).srcPh = (dt.gateBlockRule one emb args wellG setFail failPh exitPh i ρ').srcPh → ρ = ρ'

One gate block separates in-shape.

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.gatesRule_dstIn {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) {S : P → Prop} (hemb : ∀ (p : dt.GatesPh v), S (emb p)) (hfail : S failPh) (hexit : S exitPh) (i : dt.GatesSite v) (ρ : dt.GatesSh v i) : S (dt.gatesRule one v emb argsG wellGOf setFail enterSt failPh exitPh i ρ).dstPh

A property of the gates' phases, their failing exit and their exit holds of every phase they can move to.

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.

theorem DescriptiveComplexity.Draw.Data.gatesSep {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) (hemb : Function.Injective emb) (i : dt.GatesSite v) (ρ ρ' : dt.GatesSh v i) (f : Q → A) (g : dt.SlotIx → A) : (dt.gatesRule one v emb argsG wellGOf setFail enterSt failPh exitPh i ρ).guard f g → (dt.gatesRule one v emb argsG wellGOf setFail enterSt failPh exitPh i ρ').guard f g → (dt.gatesRule one v emb argsG wellGOf setFail enterSt failPh exitPh i ρ).srcPh = (dt.gatesRule one v emb argsG wellGOf setFail enterSt failPh exitPh i ρ').srcPh → ρ = ρ'

The gates separate in-shape.

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.

theorem DescriptiveComplexity.Draw.Data.igatesRule_dstIn {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) {S : P → Prop} (hemb : ∀ (p : dt.IGatesPh v), S (emb p)) (hexit : S exitPh) (i : dt.IGatesSite v) (ρ : dt.IGatesSh v i) : S (dt.igatesRule one v emb argsG wellGOf setFailOf enterSt exitPh i ρ).dstPh

A property of the inner gates' phases and their exit holds of every phase they can move to: a failing inner gate leaves into the next checkpoint, which is one of their own.

theorem DescriptiveComplexity.Draw.Data.igatesHosrc {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) : ∃ (p : dt.IGatesPh v), (dt.igatesRule one v emb argsG wellGOf setFailOf enterSt exitPh i ρ).srcPh = emb p ∧ seqOwn (fun (x : Fin (dt.nIn v)) => dt.gateBlockOwn) p = i

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

theorem DescriptiveComplexity.Draw.Data.igatesSep {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) (hemb : Function.Injective emb) (i : dt.IGatesSite v) (ρ ρ' : dt.IGatesSh v i) (f : Q → A) (g : dt.SlotIx → A) : (dt.igatesRule one v emb argsG wellGOf setFailOf enterSt exitPh i ρ).guard f g → (dt.igatesRule one v emb argsG wellGOf setFailOf enterSt exitPh i ρ').guard f g → (dt.igatesRule one v emb argsG wellGOf setFailOf enterSt exitPh i ρ).srcPh = (dt.igatesRule one v emb argsG wellGOf setFailOf enterSt exitPh i ρ').srcPh → ρ = ρ'

The inner gates separate in-shape.