The round flags, read semantically, and the pack built from the pass

The two inputs the capstone DescriptiveComplexity.Draw.Data.accVerdict_varFM_qfValue still abstracts – the flags' readings hEx/hAll and the conditional semantic pack semOf – discharged at the concrete threads:

• ctlBit_roundFX_pass_iff – a round flag at the round's exit reads as the per-polarity pass: every quantified level of that polarity holds an encoding-shaped, one-hot, domain-satisfying block. For a variable with quantified levels this is the two-flag characterization through the exit's flag ride; for one without, the flags are the constant True the VAL loop's entry seeded, riding every fold update (ctlBit_flag_varFM_of_nIn_zero).
• roundPass_of_polarities – the two readings jointly deliver the full pass, level by level – the capstone's hPass.
• passW / passW_hENC / passSem – the valuation, its master encoding fact and the semantic pack constructed from the pass: the free levels are the gated address's points, the quantified ones are chosen from DescriptiveComplexity.Draw.Data.igPassP_iff_isEnc – so the capstone's hsem is rfl.

The flags along the VAL loop, without quantified levels

The pack, built from the pass

noncomputable def DescriptiveComplexity.Draw.Data.passW {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] (RF : RegFile (Univ A R P dt.KIx dt.dd)) [Nonempty A] [L.Structure A] (zero one : A) (hzo : zero ≠ one) (hlin : IsLinOrd WMLe) (vi : dt.VarIx) (stV : TapeStD dt A R P) (hp : ∀ (ℓ : Fin (dt.nIn vi)), dt.igPassP RF 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.passW RF zero one hzo hlin vi stV hp mbW j = if h : ↑j < dt.arOf vi then mbW ⟨↑j, h⟩ else Exists.choose ⋯

theorem DescriptiveComplexity.Draw.Data.passW_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] (RF : RegFile (Univ A R P dt.KIx dt.dd)) [Nonempty A] [L.Structure A] {zero one : A} (hzo : zero ≠ one) (hlin : IsLinOrd WMLe) (vi : dt.VarIx) (stV : TapeStD dt A R P) (hp : ∀ (ℓ : Fin (dt.nIn vi)), dt.igPassP RF zero one vi stV ℓ) (mbW : Fin (dt.arOf vi) → dt.X.Map A) (hmb : ∀ (ℓ : Fin (dt.arOf vi)), wmBlk stV.mir (Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ)))) = encMap dt.ly zero one (mbW ℓ)) (j : Fin (dt.nOf vi)) : wmBlk (dt.lvSet stV vi j) (Tag.arg (toLex (dt.lvBlk vi j))) = encMap dt.ly zero one (dt.passW RF zero one hzo hlin 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.mkKindSem's input.

noncomputable def DescriptiveComplexity.Draw.Data.passSem {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] (RF : RegFile (Univ A R P dt.KIx dt.dd)) [Nonempty A] [L.Structure A] {zero one : A} (hzo : zero ≠ one) (hlin : IsLinOrd WMLe) (vi : dt.VarIx) (stV : TapeStD dt A R P) (hp : ∀ (ℓ : Fin (dt.nIn vi)), dt.igPassP RF zero one vi stV ℓ) (mbW : Fin (dt.arOf vi) → dt.X.Map A) (hmb : ∀ (ℓ : Fin (dt.arOf vi)), wmBlk stV.mir (Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ)))) = encMap dt.ly zero one (mbW ℓ)) (b : Fin (dt.natOf vi)) : dt.KindSem zero one vi stV (dt.kindOf vi b)

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

Equations

• dt.passSem RF hzo hlin vi stV hp mbW hmb b = dt.mkKindSem zero one vi stV (dt.passW RF zero one hzo hlin vi stV hp mbW) ⋯ (dt.kindOf vi b)

The stage tracks at the composed target

theorem DescriptiveComplexity.Draw.Data.old_trackOf_stageTgtD {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [LinearOrder A] [Finite A] [Nonempty A] [L.Structure A] {zero one : A} (hzo : zero ≠ one) (vi : dt.VarIx) (iv : dt.d.B.ι) (ha : dt.d.B.arity iv ≤ dt.ko) (σ : dt.d.B.Assignment (dt.X.Map A)) (stV : TapeStD dt A R P) (v : Univ A R P dt.KIx dt.dd → Prop) {Below : (Univ A R P dt.KIx dt.dd → Prop) → Prop} (hdict : ∀ (s : Univ A R P dt.KIx dt.dd → Prop), Below s → (stV.old iv s ↔ trackOf dt.ly zero one ha σ s)) (ts : Fin (dt.d.B.arity iv) → Fin (dt.nOf vi)) {p : Fin (dt.d.B.arity iv) → dt.X.Map A} (hsrc : ∀ (ℓ : Fin (dt.d.B.arity iv)), wmBlk (dt.lvSet stV vi (ts ℓ)) (Tag.arg (toLex (dt.lvBlk vi (ts ℓ)))) = encMap dt.ly zero one (p ℓ)) (hbelow : Below (dt.stageTgtD zero vi iv ts stV v (dt.d.B.arity iv))) : stV.old iv (dt.stageTgtD zero vi iv ts stV v (dt.d.B.arity iv)) ↔ σ iv p

A stage track reads the dictionary at the composed target: with the track holding the stage dictionary and the sources encoding the points, the random access's bit is the stage at those points – the capstone's hOld.

The leaf, read at the round's register