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_1) = DescriptiveComplexity.Draw.RoundSite.ig (ownG p_1)
• DescriptiveComplexity.Draw.roundOwn ownG ownX DescriptiveComplexity.Draw.RoundPh.rchk = DescriptiveComplexity.Draw.RoundSite.rchk
• DescriptiveComplexity.Draw.roundOwn ownG ownX (DescriptiveComplexity.Draw.RoundPh.matP p_1) = DescriptiveComplexity.Draw.RoundSite.mat (ownX p_1)

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 ρ

theorem DescriptiveComplexity.Draw.Data.roundRule_dstIn {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) {S : P → Prop} (hemb : ∀ (p : RoundPh PG PX), S (emb p)) (hexit : S exitPh) (hG : ∀ (s : SG) (ρ : ShG s), S (ruleG s ρ).dstPh) (hX : ∀ (s : SX) (ρ : ShX s), S (ruleX s ρ).dstPh) (hpx : S pxEntry) (i : RoundSite SG SX) (ρ : RoundSh SG SX ShG ShX i) : S (dt.roundRule one emb ruleG ruleX pxEntry exitPh existFlag allFlag i ρ).dstPh

A property of a round's phases and its exit holds of every phase it can move to, given it holds of the two sub-machineries'.

theorem DescriptiveComplexity.Draw.Data.roundHosrc {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) {ownG : PG → SG} {ownX : PX → SX} (hosrcG : ∀ (s : SG) (ρ : ShG s), ∃ (p : PG), (ruleG s ρ).srcPh = emb (RoundPh.igP p) ∧ ownG p = s) (hosrcX : ∀ (s : SX) (ρ : ShX s), ∃ (p : PX), (ruleX s ρ).srcPh = emb (RoundPh.matP p) ∧ ownX p = s) (i : RoundSite SG SX) (ρ : RoundSh SG SX ShG ShX i) : ∃ (p : RoundPh PG PX), (dt.roundRule one emb ruleG ruleX pxEntry exitPh existFlag allFlag i ρ).srcPh = emb p ∧ roundOwn ownG ownX p = i

Every rule of one round's machinery fires from a phase its site owns; the two sub-machineries' obligations are parameters.

theorem DescriptiveComplexity.Draw.Data.roundSep {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) (hsepG : ∀ (s : SG) (ρ ρ' : ShG s) (f : Q → A) (g : dt.SlotIx → A), (ruleG s ρ).guard f g → (ruleG s ρ').guard f g → (ruleG s ρ).srcPh = (ruleG s ρ').srcPh → ρ = ρ') (hsepX : ∀ (s : SX) (ρ ρ' : ShX s) (f : Q → A) (g : dt.SlotIx → A), (ruleX s ρ).guard f g → (ruleX s ρ').guard f g → (ruleX s ρ).srcPh = (ruleX s ρ').srcPh → ρ = ρ') (i : RoundSite SG SX) (ρ ρ' : RoundSh SG SX ShG ShX i) (f : Q → A) (g : dt.SlotIx → A) : (dt.roundRule one emb ruleG ruleX pxEntry exitPh existFlag allFlag i ρ).guard f g → (dt.roundRule one emb ruleG ruleX pxEntry exitPh existFlag allFlag i ρ').guard f g → (dt.roundRule one emb ruleG ruleX pxEntry exitPh existFlag allFlag i ρ).srcPh = (dt.roundRule one emb ruleG ruleX pxEntry exitPh existFlag allFlag i ρ').srcPh → ρ = ρ'

One round's machinery separates in-shape: the sub-machineries by their own separations, the checkpoint by its guards.