One round of the VAL loop: inner gates, branch, matrix

The leaf the VAL loop folds is the gated matrix (DescriptiveComplexity.Draw.Data.leafP): every ∃-level of the register must hold an encoding, and only if every ∀-level does is the matrix read. The machinery of a round therefore runs, before the matrix pass, one gate block per quantified level of the variable's pack – at the Sum.inr blocks of the VAL register – conjoining each level's verdict into one of two flags by the level's polarity, and a branch checkpoint then either enters the matrix (both flags set: every block the atoms read is an encoding, which is what their semantic packs require) or skips it. The stale verdict slots a skip leaves behind are harmless: the leaf is exist ∧ (all → matrix), decided by the flags alone whenever the matrix did not run.

This composite is slotted into the matrix parameter of DescriptiveComplexity.Draw.Data.varRule – which is generic in its PX/SX types and enters them only through pxEntry – so the variable machinery, its run theorem and everything above them are untouched.

Shapes only; the runs are the instantiation files'.

The shapes

inductive DescriptiveComplexity.Draw.RoundPh (PG PX : Type) : Type

The phases of one round's machinery: the inner gates, the branch checkpoint, and the matrix.

• igP {PG PX : Type} : PG → RoundPh PG PX

  A phase of the inner gates.

• rchk {PG PX : Type} : RoundPh PG PX

  The branch checkpoint: dispatch on the two gate flags.

• matP {PG PX : Type} : PX → RoundPh PG PX

  A phase of the matrix.

instance DescriptiveComplexity.Draw.instFiniteRoundPh {PG PX : Type} [Finite PG] [Finite PX] : Finite (RoundPh PG PX)

inductive DescriptiveComplexity.Draw.RoundSite (SG SX : Type) : Type

The sites of one round's machinery.

• ig {SG SX : Type} : SG → RoundSite SG SX

  An inner-gates site.

• rchk {SG SX : Type} : RoundSite SG SX

  The branch checkpoint.

• mat {SG SX : Type} : SX → RoundSite SG SX

  A matrix site.

instance DescriptiveComplexity.Draw.instFiniteRoundSite {SG SX : Type} [Finite SG] [Finite SX] : Finite (RoundSite SG SX)

def DescriptiveComplexity.Draw.RoundSh (SG SX : Type) (ShG : SG → Type) (ShX : SX → Type) : RoundSite SG SX → Type

The rule shape of each site: the checkpoint's the three-rule gadget of the spine layer.

Equations

• DescriptiveComplexity.Draw.RoundSh SG SX ShG ShX (DescriptiveComplexity.Draw.RoundSite.ig s) = ShG s
• DescriptiveComplexity.Draw.RoundSh SG SX ShG ShX DescriptiveComplexity.Draw.RoundSite.rchk = DescriptiveComplexity.Draw.EvalChkRule
• DescriptiveComplexity.Draw.RoundSh SG SX ShG ShX (DescriptiveComplexity.Draw.RoundSite.mat s) = ShX s

def DescriptiveComplexity.Draw.roundOwn {PG PX SG SX : Type} (ownG : PG → SG) (ownX : PX → SX) : RoundPh PG PX → RoundSite SG SX

The owner of each phase, over the sub-machineries' owners.

Equations

• DescriptiveComplexity.Draw.roundOwn ownG ownX (DescriptiveComplexity.Draw.RoundPh.igP p) = DescriptiveComplexity.Draw.RoundSite.ig (ownG p)
• DescriptiveComplexity.Draw.roundOwn ownG ownX DescriptiveComplexity.Draw.RoundPh.rchk = DescriptiveComplexity.Draw.RoundSite.rchk
• DescriptiveComplexity.Draw.roundOwn ownG ownX (DescriptiveComplexity.Draw.RoundPh.matP p) = DescriptiveComplexity.Draw.RoundSite.mat (ownX p)

noncomputable def DescriptiveComplexity.Draw.Data.roundRule {L : FirstOrder.Language} (dt : Data L) {A Q P PG PX SG SX : Type} (one : A) {ShG : SG → Type} {ShX : SX → Type} (emb : RoundPh PG PX → P) (ruleG : (s : SG) → ShG s → Rule A Q dt.SlotIx P) (ruleX : (s : SX) → ShX s → Rule A Q dt.SlotIx P) (pxEntry exitPh : P) (existFlag allFlag : Q) (i : RoundSite SG SX) : RoundSh SG SX ShG ShX i → Rule A Q dt.SlotIx P

The rules of one round's machinery. Parameters: the phase embedding, the two sub-machineries, the matrix's entry, the exit phase (the variable's post-matrix checkpoint – reached through the matrix or by the skip), and the two gate flags.

Equations

• One or more equations did not get rendered due to their size.
• dt.roundRule one emb ruleG ruleX pxEntry exitPh existFlag allFlag (DescriptiveComplexity.Draw.RoundSite.ig s) ρ = ruleG s ρ
• dt.roundRule one emb ruleG ruleX pxEntry exitPh existFlag allFlag (DescriptiveComplexity.Draw.RoundSite.mat s) ρ = ruleX s ρ