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

theorem DescriptiveComplexity.Draw.Data.ctlBit_flag_varFM_of_nIn_zero {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R P dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] {vi : dt.VarIx} {st : TapeStD dt A R P} {ιV : Type} [LinearOrder ιV] [Finite ιV] {mV : ιV → Univ A R P dt.KIx dt.dd → Prop} {semOf : (a : ιV) → (∀ (ℓ : Fin (dt.nIn vi)), dt.igPassP RF PR.zero PR.one vi (dt.roundSt st (mV a)) ℓ) → (b : Fin (dt.natOf vi)) → dt.KindSem PR.zero PR.one vi (dt.roundSt st (mV a)) (dt.kindOf vi b)} (hzo : PR.zero ≠ PR.one) (hn0 : dt.nIn vi = 0) {q : dt.CtlIx} (hq : q = dt.existGateC ∨ q = dt.allGateC) (v : Univ A R P dt.KIx dt.dd → Prop) (fG : dt.CtlIx → A) (a : ιV) : dt.ctlBit PR.one (varFM RF hord vi st v mV semOf fG a) q

Without quantified levels the two flags are constant along the VAL loop: the entry seeded them True, the inner-gates thread is empty, and no fold update writes a flag.

theorem DescriptiveComplexity.Draw.Data.ctlBit_roundFX_pass_iff {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R P dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] {vi : dt.VarIx} {st : TapeStD dt A R P} {ιV : Type} [LinearOrder ιV] [Finite ιV] {mV : ιV → Univ A R P dt.KIx dt.dd → Prop} {semOf : (a : ιV) → (∀ (ℓ : Fin (dt.nIn vi)), dt.igPassP RF PR.zero PR.one vi (dt.roundSt st (mV a)) ℓ) → (b : Fin (dt.natOf vi)) → dt.KindSem PR.zero PR.one vi (dt.roundSt st (mV a)) (dt.kindOf vi b)} (hzo : PR.zero ≠ PR.one) {q : dt.CtlIx} (hq : q = dt.existGateC ∨ q = dt.allGateC) (v : Univ A R P dt.KIx dt.dd → Prop) (fG : dt.CtlIx → A) (a : ιV) : dt.ctlBit PR.one (roundFX RF hord vi st v mV semOf (varFM RF hord vi st v mV semOf fG a) a) q ↔ ∀ (ℓ : Fin (dt.nIn vi)), dt.igFlag vi ℓ = q → dt.igPassP RF PR.zero PR.one vi (dt.roundSt st (mV a)) ℓ

A round flag at the round's exit reads as the per-polarity pass: every quantified level of the flag's polarity holds an encoding-shaped, one-hot, domain-satisfying block value. The capstone's hEx/hAll.

theorem DescriptiveComplexity.Draw.Data.roundPass_of_polarities {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] {vi : dt.VarIx} {zero one : A} {stV : TapeStD dt A R P} (hEx : ∀ (ℓ : Fin (dt.nIn vi)), dt.igFlag vi ℓ = dt.existGateC → dt.igPassP RF zero one vi stV ℓ) (hAl : ∀ (ℓ : Fin (dt.nIn vi)), dt.igFlag vi ℓ = dt.allGateC → dt.igPassP RF zero one vi stV ℓ) (ℓ : Fin (dt.nIn vi)) : dt.igPassP RF zero one vi stV ℓ

The two polarity readings deliver the full pass: every level's flag is one of the two. The capstone's hPass.

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.wmBlk_stageTgtD_eq_encMap {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [LinearOrder A] [Finite A] [Nonempty A] [L.Structure A] {zero one : A} (vi : dt.VarIx) (iv : dt.d.B.ι) (ts : Fin (dt.d.B.arity iv) → Fin (dt.nOf vi)) (stV : TapeStD dt A R P) (v : Univ A R P dt.KIx dt.dd → Prop) {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 ℓ)) (ℓ : Fin (dt.d.B.arity iv)) : wmBlk (dt.stageTgtD zero vi iv ts stV v (dt.d.B.arity iv)) (Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ)))) = encMap dt.ly zero one (p ℓ)

The composed TARGET's argument blocks are the sources': after all copy loops, block ℓ of TARGET is the position's source block – the copy is faithful on the padded cells, and an encoding holds no others.

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

theorem DescriptiveComplexity.Draw.Data.igFlag_eq_existGateC_iff {L : FirstOrder.Language} (dt : Data L) (vi : dt.VarIx) (ℓ : Fin (dt.nIn vi)) : dt.igFlag vi ℓ = dt.existGateC ↔ dt.polOf vi (dt.arOf vi + ↑ℓ) = true

A level's polarity flag is the ∃-flag exactly by its polarity.

theorem DescriptiveComplexity.Draw.Data.igFlag_eq_allGateC_iff {L : FirstOrder.Language} (dt : Data L) (vi : dt.VarIx) (ℓ : Fin (dt.nIn vi)) : dt.igFlag vi ℓ = dt.allGateC ↔ dt.polOf vi (dt.arOf vi + ↑ℓ) = false

A level's polarity flag is the ∀-flag exactly by its polarity.

theorem DescriptiveComplexity.Draw.Data.roundPass_iff_split_gen {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) {q : dt.CtlIx} {bpol : Bool} (hqiff : ∀ (ℓ : Fin (dt.nIn vi)), dt.igFlag vi ℓ = q ↔ dt.polOf vi (dt.arOf vi + ↑ℓ) = bpol) : (∀ (ℓ : Fin (dt.nIn vi)), dt.igFlag vi ℓ = q → dt.igPassP RF zero one vi stV ℓ) ↔ ∀ (j : Fin (dt.nOf vi)), dt.arOf vi ≤ ↑j → dt.polOf vi ↑j = bpol → IsEnc dt.ly zero one (ixBlk (argIn dt.ko) stV.val ⟨↑j, ⋯⟩)

A per-polarity pass is the split's gate clause, reindexed from the quantified levels to the pack's indices.

theorem DescriptiveComplexity.Draw.Data.levelVal_encMap {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 ℓ) (mb : Fin dt.ko → (Fin dt.dd → A) → Prop) (mbW : Fin (dt.arOf vi) → dt.X.Map A) (hmb : ∀ (ℓ : Fin (dt.arOf vi)), mb (Fin.castLE ⋯ ℓ) = encMap dt.ly zero one (mbW ℓ)) (j : Fin (dt.nOf vi)) : dt.levelVal vi mb (ixBlk (argIn dt.ko) stV.val) j = encMap dt.ly zero one (dt.passW RF zero one hzo hlin vi stV hp mbW j)

The valuation the leaf decodes is the pass's: every level's block of the leaf's reading encodes passW's point.

theorem DescriptiveComplexity.Draw.Data.leafP_pass_iff {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} [LinearOrder (dt.X.Map A)] (hzo : zero ≠ one) (hlin : IsLinOrd WMLe) (vi : dt.VarIx) (stV : TapeStD dt A R P) (σ : dt.d.B.Assignment (dt.X.Map A)) (mb : Fin dt.ko → (Fin dt.dd → A) → Prop) (mbW : Fin (dt.arOf vi) → dt.X.Map A) (hmb : ∀ (ℓ : Fin (dt.arOf vi)), mb (Fin.castLE ⋯ ℓ) = encMap dt.ly zero one (mbW ℓ)) (hp : ∀ (ℓ : Fin (dt.nIn vi)), dt.igPassP RF zero one vi stV ℓ) : dt.leafP zero one vi σ mb (ixBlk (argIn dt.ko) stV.val) ↔ qfValue (dt.matOf vi) fun (atm : ((dt.X.E.sum FirstOrder.Language.order).sum dt.d.B.lang).BoundedFormula Empty (dt.nOf vi)) => (matAtom? atm).elim False (MatAtom.holds σ (dt.passW RF zero one hzo hlin vi stV hp mbW))

The leaf at a passing round is the matrix's value at the pass's points – the capstone's hPsPass, with Ps the gated matrix DescriptiveComplexity.Draw.Data.leafP.

theorem DescriptiveComplexity.Draw.Data.leafP_fail_iff {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} [LinearOrder (dt.X.Map A)] (hzo : zero ≠ one) (hlin : IsLinOrd WMLe) (vi : dt.VarIx) (stV : TapeStD dt A R P) (σ : dt.d.B.Assignment (dt.X.Map A)) (mb : Fin dt.ko → (Fin dt.dd → A) → Prop) (mbW : Fin (dt.arOf vi) → dt.X.Map A) (hmb : ∀ (ℓ : Fin (dt.arOf vi)), mb (Fin.castLE ⋯ ℓ) = encMap dt.ly zero one (mbW ℓ)) (hEA : ¬((∀ (ℓ : Fin (dt.nIn vi)), dt.igFlag vi ℓ = dt.existGateC → dt.igPassP RF zero one vi stV ℓ) ∧ ∀ (ℓ : Fin (dt.nIn vi)), dt.igFlag vi ℓ = dt.allGateC → dt.igPassP RF zero one vi stV ℓ)) : (∀ (ℓ : Fin (dt.nIn vi)), dt.igFlag vi ℓ = dt.existGateC → dt.igPassP RF zero one vi stV ℓ) ↔ dt.leafP zero one vi σ mb (ixBlk (argIn dt.ko) stV.val)

The leaf at a failing round is the ∃-clause alone – the capstone's hPsFail: the ∀-clause's implication is vacuous when the two readings do not both hold.