The round flags and the pass's pack, at an arbitrary file

DescriptiveComplexity.Problems.Wide.DrawRoundSem read at a coarse file: the flags' semantic readings, the pass they jointly deliver, the valuation and the semantic pack built from it, and the leaf's two readings.

The flags along the VAL loop, without quantified levels

The pack, built from the pass

noncomputable def DescriptiveComplexity.Draw.Data.ixPassW {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] {I : Type} (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} [Nonempty A] [L.Structure A] (zero one : A) (hpassEnc : ∀ (vi : dt.VarIx) (stV : TapeSt dt A R P I) (ℓ : Fin (dt.nIn vi)), dt.ixIGPassP F zero one vi stV ℓ ↔ IsEnc dt.ly zero one (wmBlk (ixAddr elt stV.val) (Tag.arg (toLex (dt.igBlk vi ℓ))))) (vi : dt.VarIx) (stV : TapeSt dt A R P I) (hp : ∀ (ℓ : Fin (dt.nIn vi)), dt.ixIGPassP F zero one vi stV ℓ) (mbW : Fin (dt.arOf vi) → dt.X.Map A) (j : Fin (dt.nOf vi)) : dt.X.Map A

The valuation a passing round holds: the gated address's points at the free levels, the points the pass's encodings choose at the quantified ones.

Equations

• dt.ixPassW F zero one hpassEnc vi stV hp mbW j = if h : ↑j < dt.arOf vi then mbW ⟨↑j, h⟩ else Exists.choose ⋯

theorem DescriptiveComplexity.Draw.Data.ixPassW_hENC {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] {I : Type} (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} [Nonempty A] [L.Structure A] {zero one : A} (hpassEnc : ∀ (vi : dt.VarIx) (stV : TapeSt dt A R P I) (ℓ : Fin (dt.nIn vi)), dt.ixIGPassP F zero one vi stV ℓ ↔ IsEnc dt.ly zero one (wmBlk (ixAddr elt stV.val) (Tag.arg (toLex (dt.igBlk vi ℓ))))) (vi : dt.VarIx) (stV : TapeSt dt A R P I) (hp : ∀ (ℓ : Fin (dt.nIn vi)), dt.ixIGPassP F zero one vi stV ℓ) (mbW : Fin (dt.arOf vi) → dt.X.Map A) (hmb : ∀ (ℓ : Fin (dt.arOf vi)), wmBlk (ixAddr elt stV.mir) (Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ)))) = encMap dt.ly zero one (mbW ℓ)) (j : Fin (dt.nOf vi)) : wmBlk (ixAddr elt (dt.lvSet stV vi j)) (Tag.arg (toLex (dt.lvBlk vi j))) = encMap dt.ly zero one (dt.ixPassW F zero one hpassEnc vi stV hp mbW j)

The master encoding fact of a passing round: every level's block – the working address's at the free levels, the round register's at the quantified ones – encodes the valuation's point. The capstone's hENC, and DescriptiveComplexity.Draw.Data.ixMkKindSem's input.

noncomputable def DescriptiveComplexity.Draw.Data.ixPassSem {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] {I : Type} (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} [Nonempty A] [L.Structure A] {zero one : A} (hpassEnc : ∀ (vi : dt.VarIx) (stV : TapeSt dt A R P I) (ℓ : Fin (dt.nIn vi)), dt.ixIGPassP F zero one vi stV ℓ ↔ IsEnc dt.ly zero one (wmBlk (ixAddr elt stV.val) (Tag.arg (toLex (dt.igBlk vi ℓ))))) (vi : dt.VarIx) (stV : TapeSt dt A R P I) (hp : ∀ (ℓ : Fin (dt.nIn vi)), dt.ixIGPassP F zero one vi stV ℓ) (mbW : Fin (dt.arOf vi) → dt.X.Map A) (hmb : ∀ (ℓ : Fin (dt.arOf vi)), wmBlk (ixAddr elt stV.mir) (Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ)))) = encMap dt.ly zero one (mbW ℓ)) (b : Fin (dt.natOf vi)) : dt.IxKindSem zero one vi stV elt (dt.kindOf vi b)

The semantic pack of a passing round, constructed: the capstone's semOf, with hsem definitional.

Equations

• dt.ixPassSem F hpassEnc vi stV hp mbW hmb b = dt.ixMkKindSem zero one vi stV (dt.ixPassW F zero one hpassEnc vi stV hp mbW) ⋯ (dt.kindOf vi b)

The stage tracks at the composed target

The leaf, read at the round's register