One round of the VAL loop, assembled

The composite DescriptiveComplexity.Draw.RoundPh slotted into the variable machinery's matrix parameter, run end to end: the inner gates – one gate block per quantified level of the variable's pack, at the Sum.inr blocks of the VAL register, each level's verdict conjoined into its polarity's flag and a failing level continuing – the branch checkpoint dispatching on the two flags, and the matrix pass on the passing branch only.

Two levels here. DescriptiveComplexity.Draw.Data.igateBlock_hStage_pos / _neg are one level's stage in the sequencer's shape – the mirrors of the outer DescriptiveComplexity.Draw.Data.gateBlock_hStage_pos/_neg at the igateArgs pack, the failing exit continuing to the next checkpoint. DescriptiveComplexity.Draw.Data.igFs is the concrete control thread over the levels – pass or fail decided classically by the level's file-test question DescriptiveComplexity.Draw.Data.igTest – DescriptiveComplexity.Draw.Data.igs_run its run, and DescriptiveComplexity.Draw.Data.round_run the whole round at the program's own rules: inner gates, branch, matrix or skip, ending at the fold checkpoint with DescriptiveComplexity.Draw.Data.roundCtl – the matrix thread applied to the gates' output at a passing round, the gates' output alone otherwise.

No semantic hypothesis survives: the pass/fail of a level and the branch of the checkpoint are decided classically inside the statements, which is what lets the round hypothesis of DescriptiveComplexity.Draw.Data.varMachine_run be discharged for every VAL content the loop enumerates.

One inner gate block, in the sequencer's shape

theorem DescriptiveComplexity.Draw.Data.igateBlock_hStage_pos {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] [Finite R] [Finite P] {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] (b : Fin dt.ko ⊕ Fin dt.ki) (flag : dt.CtlIx) (hc : Fintype.card dt.X.Tag ≤ dt.ntgDim) (hn : ∀ (t' : dt.X.Tag), (dt.domPk t').n ≤ dt.eDim) (hrd : ∀ (t' : dt.X.Tag), dt.domNr t' ≤ dt.nfDim) {emb : dt.GateBlockPh → P} (wellG : (dt.SlotIx → A) → Prop) (setFail : (dt.CtlIx → A) → (dt.SlotIx → A) → dt.CtlIx → A) {failPh exitPh : P} {rEmb : (i : dt.GateBlockSite) → dt.GateBlockSh i → R} [Finite dt.KIx] (hrules : ∀ (i : dt.GateBlockSite) (ρ : dt.GateBlockSh i), PR.rules (rEmb i ρ) = dt.gateBlockRule PR.one emb (dt.igateArgs PR.zero PR.one b flag hc hn hrd) wellG setFail failPh exitPh i ρ) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) {gtop gbot : Univ A R P dt.KIx dt.dd} (htop : ∀ (y : Univ A R P dt.KIx dt.dd), WMLe y gtop) (hbot : ∀ (y : Univ A R P dt.KIx dt.dd), WMLe gbot y) {v v' : Univ A R P dt.KIx dt.dd → Prop} (hv : WMSetLt WMLe v (RF.cell gbot)) (hvi : WMIncr WMLe v v') {st : TapeStD dt A R P} (hwkSt : st.wk = fun (r : Univ A R P dt.KIx dt.dd → Prop) => r = v) (Test : Univ A R P dt.KIx dt.dd → Prop) (hcompat : ∀ (u : Univ A R P dt.KIx dt.dd), wellG (PR.passTracksAt RF.cell Slot.mir (dt.back RF.cell PR.zero PR.one ⋯ st) st.mir (RF.cell u)) ↔ Test u) (hTest : ∀ (u : Univ A R P dt.KIx dt.dd), Test u) (f : dt.CtlIx → A) : Relation.ReflTransGen (wideData (Univ A R P dt.KIx dt.dd)).Step { state := Sum.inr (PR.stElt (emb (Sum.inl TestPh.up)) f), head := Sum.inl v', tape := wideTape (PR.trackTapeAt RF.cell Slot.val (dt.back RF.cell PR.zero PR.one ⋯ st) st.val) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt exitPh ((dt.igateArgs PR.zero PR.one b flag hc hn hrd).exitSt (dt.dspTagOf PR.zero PR.one (wmBlk st.val (Tag.arg (toLex b)))) (dt.igateFam RF PR.zero PR.one b st (dt.dspTagOf PR.zero PR.one (wmBlk st.val (Tag.arg (toLex b)))) flag hc hn hrd v (dt.igateTagFam RF PR.zero PR.one b st flag hc hn hrd v f (Fin.last (Fintype.card dt.X.Tag))) (toLex topTup) (Fin.last (dt.domNr (dt.dspTagOf PR.zero PR.one (wmBlk st.val (Tag.arg (toLex b))))))) (dt.back RF.cell PR.zero PR.one ⋯ st v))), head := Sum.inl v', tape := wideTape (PR.trackTapeAt RF.cell Slot.val (dt.back RF.cell PR.zero PR.one ⋯ st) st.val) (PR.syElt PR.blank) }

A passing inner gate block, entered by a dispatch: the file test passes, the witness chain reads the VAL block, the branch dispatches – on the decoded tag or the default – the domain loop runs, and the conjoining exit lands at the next checkpoint.

theorem DescriptiveComplexity.Draw.Data.igateBlock_hStage_neg {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] [Finite R] [Finite P] {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] (b : Fin dt.ko ⊕ Fin dt.ki) (flag : dt.CtlIx) (hc : Fintype.card dt.X.Tag ≤ dt.ntgDim) (hn : ∀ (t' : dt.X.Tag), (dt.domPk t').n ≤ dt.eDim) (hrd : ∀ (t' : dt.X.Tag), dt.domNr t' ≤ dt.nfDim) {emb : dt.GateBlockPh → P} (wellG : (dt.SlotIx → A) → Prop) (setFail : (dt.CtlIx → A) → (dt.SlotIx → A) → dt.CtlIx → A) {failPh exitPh : P} {rEmb : (i : dt.GateBlockSite) → dt.GateBlockSh i → R} [Finite dt.KIx] (hrules : ∀ (i : dt.GateBlockSite) (ρ : dt.GateBlockSh i), PR.rules (rEmb i ρ) = dt.gateBlockRule PR.one emb (dt.igateArgs PR.zero PR.one b flag hc hn hrd) wellG setFail failPh exitPh i ρ) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) {gtop gbot : Univ A R P dt.KIx dt.dd} (htop : ∀ (y : Univ A R P dt.KIx dt.dd), WMLe y gtop) (hbot : ∀ (y : Univ A R P dt.KIx dt.dd), WMLe gbot y) {v v' : Univ A R P dt.KIx dt.dd → Prop} (hv : WMSetLt WMLe v (RF.cell gbot)) (hvi : WMIncr WMLe v v') {st : TapeStD dt A R P} (hwkSt : st.wk = fun (r : Univ A R P dt.KIx dt.dd → Prop) => r = v) (Test : Univ A R P dt.KIx dt.dd → Prop) (hcompat : ∀ (u : Univ A R P dt.KIx dt.dd), wellG (PR.passTracksAt RF.cell Slot.mir (dt.back RF.cell PR.zero PR.one ⋯ st) st.mir (RF.cell u)) ↔ Test u) {u : Univ A R P dt.KIx dt.dd} (hTest : ¬Test u) (f : dt.CtlIx → A) : Relation.ReflTransGen (wideData (Univ A R P dt.KIx dt.dd)).Step { state := Sum.inr (PR.stElt (emb (Sum.inl TestPh.up)) f), head := Sum.inl v', tape := wideTape (PR.trackTapeAt RF.cell Slot.val (dt.back RF.cell PR.zero PR.one ⋯ st) st.val) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt failPh (setFail f (dt.back RF.cell PR.zero PR.one ⋯ st v))), head := Sum.inl v', tape := wideTape (PR.trackTapeAt RF.cell Slot.val (dt.back RF.cell PR.zero PR.one ⋯ st) st.val) (PR.syElt PR.blank) }

A failing inner gate block: some register cell is not well-shaped, so the file test fails and the block leaves through the failing exit – for an inner gate, the next checkpoint – with the fail store applied at the marker's symbol.

The concrete thread over the levels

theorem DescriptiveComplexity.Draw.Data.domN {L : FirstOrder.Language} (dt : Data L) (t : dt.X.Tag) : (dt.domPk t).n ≤ dt.eDim

The domain-sentence depth budget, packaged.

theorem DescriptiveComplexity.Draw.Data.domRd {L : FirstOrder.Language} (dt : Data L) (t : dt.X.Tag) : dt.domNr t ≤ dt.nfDim

The domain-sentence read budget, packaged.

noncomputable def DescriptiveComplexity.Draw.Data.igBlk {L : FirstOrder.Language} (dt : Data L) (vi : dt.VarIx) (ℓ : Fin (dt.nIn vi)) : Fin dt.ko ⊕ Fin dt.ki

The inner block of a quantified level: the Sum.inr block the level's point occupies.

Equations

• dt.igBlk vi ℓ = Sum.inr ⟨dt.arOf vi + ↑ℓ, ⋯⟩

noncomputable def DescriptiveComplexity.Draw.Data.igFlag {L : FirstOrder.Language} (dt : Data L) (vi : dt.VarIx) (ℓ : Fin (dt.nIn vi)) : dt.CtlIx

The polarity flag of a quantified level.

Equations

• dt.igFlag vi ℓ = if dt.polOf vi (dt.arOf vi + ↑ℓ) = true then dt.existGateC else dt.allGateC

noncomputable def DescriptiveComplexity.Draw.Data.igTest {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)] (RF : RegFile (Univ A R P dt.KIx dt.dd)) (zero one : A) (stV : TapeStD dt A R P) (b : Fin dt.ko ⊕ Fin dt.ki) (u : Univ A R P dt.KIx dt.dd) : Prop

The file-test question of an inner gate, semantically: every cell of the gated block that the round's register holds is encoding-shaped.

Equations

• dt.igTest RF zero one stV b u = dt.wellShapedIG zero one b (dt.back RF.cell zero one ⋯ stV (RF.cell u))

theorem DescriptiveComplexity.Draw.Data.wellShapedIG_congr {L : FirstOrder.Language} (dt : Data L) {A : Type} (zero one : A) (b : Fin dt.ko ⊕ Fin dt.ki) {g g' : dt.SlotIx → A} (hblk : g (Slot.blk (some b)) = g' (Slot.blk (some b))) (hval : g Slot.val = g' Slot.val) (hpdd : g Slot.pdd = g' Slot.pdd) (hname : ∀ (j : Fin dt.dd0), g (Slot.name j) = g' (Slot.name j)) : dt.wellShapedIG zero one b g ↔ dt.wellShapedIG zero one b g'

A gate's file test reads four slots: the block mark, the VAL digit, the padding mark and the name slots.

theorem DescriptiveComplexity.Draw.Data.igTest_congr {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)] (RF : RegFile (Univ A R P dt.KIx dt.dd)) (zero one : A) {st st' : TapeStD dt A R P} (hval : st.val = st'.val) (b : Fin dt.ko ⊕ Fin dt.ki) (u : Univ A R P dt.KIx dt.dd) : dt.igTest RF zero one st b u ↔ dt.igTest RF zero one st' b u

A file test depends on the VAL register alone: everything else it reads is the tape's permanent geometry.

noncomputable def DescriptiveComplexity.Draw.Data.igFs {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.IsRelational] [L.Structure A] (zero one : A) (vi : dt.VarIx) (stV : TapeStD dt A R P) (v : Univ A R P dt.KIx dt.dd → Prop) (f₀ : dt.CtlIx → A) : ℕ → dt.CtlIx → A

The control thread across one round's inner gates: each level's machinery entered through the pack's enterIGSt – the first level resetting the two flags – its conjoining exit the next level's input where the file test passes, the fail store where it does not.

Equations

• One or more equations did not get rendered due to their size.
• dt.igFs RF zero one vi stV v f₀ 0 = f₀

theorem DescriptiveComplexity.Draw.Data.igFs_congr_scratch {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.IsRelational] [L.Structure A] (zero one : A) {v : Univ A R P dt.KIx dt.dd → Prop} {stV stV' : TapeStD dt A R P} (h : dt.ScratchEq stV stV') (hreg : ¬∃ (u : Univ A R P dt.KIx dt.dd), v = RF.cell u) (vi : dt.VarIx) (f₀ : dt.CtlIx → A) (n : ℕ) : dt.igFs RF zero one vi stV v f₀ n = dt.igFs RF zero one vi stV' v f₀ n

The inner gates are blind to the two scratch registers: every level's test reads the VAL register (igTest_congr), its dispatched tag is that register's block value, and its two loops read their background at the working cell.

noncomputable def DescriptiveComplexity.Draw.Data.igPassP {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) (vi : dt.VarIx) (stV : TapeStD dt A R P) (ℓ : Fin (dt.nIn vi)) : Prop

What one level's gate is worth: the file test passed, the block value's witness one-hot at the dispatched tag, and the domain condition there. By DescriptiveComplexity.Draw.Data.igVerdict_iff_isEnc this is IsEnc of the block value, once the encoding layer relates the test's marks to the true shapes.

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.Draw.Data.igPassP_congr {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) (vi : dt.VarIx) {st st' : TapeStD dt A R P} (hval : st.val = st'.val) (ℓ : Fin (dt.nIn vi)) : dt.igPassP RF zero one vi st ℓ ↔ dt.igPassP RF zero one vi st' ℓ

A round's pass depends on the VAL register alone. Hence at a round state (DescriptiveComplexity.Draw.Data.roundSt, which sets VAL and keeps everything else) the pass is the same proposition at every position of the spine – so a position's hp is the entry state's, and kindSemCast may carry the pack it unlocks.

The rides: what the round's machinery never writes

theorem DescriptiveComplexity.Draw.Data.igFs_apply_accC {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.IsRelational] [L.Structure A] {zero one : A} (vi : dt.VarIx) (stV : TapeStD dt A R P) (v : Univ A R P dt.KIx dt.dd → Prop) (f₀ : dt.CtlIx → A) (jj : Fin dt.naDim) (n : ℕ) : dt.igFs RF zero one vi stV v f₀ n (dt.accC jj) = f₀ (dt.accC jj)

The inner fold's vector survives the inner gates: no level's machinery – witness chain, domain loop, conjoining exit, fail store or entry reset – ever writes an accumulator.

theorem DescriptiveComplexity.Draw.Data.kindExitCtl_apply_roundFlag {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)) (hord : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] {zero one : A} {q : dt.CtlIx} (hq : q = dt.existGateC ∨ q = dt.allGateC) (vi : dt.VarIx) (av : Fin dt.natMax) (st : TapeStD dt A R P) (v : Univ A R P dt.KIx dt.dd → Prop) (κ : MatAtom dt.X dt.d.B (dt.nOf vi)) (sem : dt.KindSem zero one vi st κ) (hk : dt.kindArgs κ * Fintype.card dt.X.Tag ≤ dt.ntgDim) (hnd : dt.kindDepth κ ≤ dt.eDim) (hrd : dt.kindReads κ ≤ dt.nfDim) (f : dt.CtlIx → A) : dt.kindExitCtl RF hord zero one vi av st v κ sem hk hnd hrd f q = f q

A round flag survives one atom's machinery: no kind's exit control writes the two VAL-round gate flags.

theorem DescriptiveComplexity.Draw.Data.matFs_apply_roundFlag {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)) (hord : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] {zero one : A} {q : dt.CtlIx} (hq : q = dt.existGateC ∨ q = dt.allGateC) (vi : dt.VarIx) (st : TapeStD dt A R P) (v : Univ A R P dt.KIx dt.dd → Prop) (sem : (b : Fin (dt.natOf vi)) → dt.KindSem zero one vi st (dt.kindOf vi b)) (f₀ : dt.CtlIx → A) (n : ℕ) : dt.matFs RF hord zero one vi st v (dt.varArgsOf zero one vi).enterAtomSt sem f₀ n q = f₀ q

A round flag survives the whole matrix: what the branch checkpoint read, the fold checkpoint still reads.

The two-flag characterization

theorem DescriptiveComplexity.Draw.Data.ctlBit_flag_igFs_succ {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.IsRelational] [L.Structure A] {zero one : A} (hzo : zero ≠ one) {q : dt.CtlIx} (hq : q = dt.existGateC ∨ q = dt.allGateC) (vi : dt.VarIx) (stV : TapeStD dt A R P) (v : Univ A R P dt.KIx dt.dd → Prop) (f₀ : dt.CtlIx → A) {n : ℕ} (hℓn : n < dt.nIn vi) : dt.ctlBit one (dt.igFs RF zero one vi stV v f₀ (n + 1)) q ↔ dt.ctlBit one ((dt.varArgsOf zero one vi).enterIGSt ⟨n, hℓn⟩ (dt.igFs RF zero one vi stV v f₀ n) (dt.back RF.cell zero one ⋯ stV v)) q ∧ (dt.igFlag vi ⟨n, hℓn⟩ = q → dt.igPassP RF zero one vi stV ⟨n, hℓn⟩)

One level's effect on a round flag: its own polarity flag becomes “held at entry ∧ the level's verdict”; the other polarity's rides through.

theorem DescriptiveComplexity.Draw.Data.ctlBit_flag_igFs {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.IsRelational] [L.Structure A] {zero one : A} (hzo : zero ≠ one) {q : dt.CtlIx} (hq : q = dt.existGateC ∨ q = dt.allGateC) (vi : dt.VarIx) (stV : TapeStD dt A R P) (v : Univ A R P dt.KIx dt.dd → Prop) (f₀ : dt.CtlIx → A) {n : ℕ} (h1 : 1 ≤ n) (hn : n ≤ dt.nIn vi) : dt.ctlBit one (dt.igFs RF zero one vi stV v f₀ n) q ↔ ∀ (ℓ : Fin (dt.nIn vi)), ↑ℓ < n → dt.igFlag vi ℓ = q → dt.igPassP RF zero one vi stV ℓ

The two-flag characterization: after the whole inner-gates thread, a round flag holds exactly when every quantified level of its polarity passes its gate – the file test, the one-hot witness at the dispatched tag, and the domain condition there.

theorem DescriptiveComplexity.Draw.Data.roundPass_of_flags {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.IsRelational] [L.Structure A] {zero one : A} (hzo : zero ≠ one) (vi : dt.VarIx) (stV : TapeStD dt A R P) (v : Univ A R P dt.KIx dt.dd → Prop) (f₀ : dt.CtlIx → A) (h : dt.ctlBit one (dt.igFs RF zero one vi stV v f₀ (dt.nIn vi)) dt.existGateC ∧ dt.ctlBit one (dt.igFs RF zero one vi stV v f₀ (dt.nIn vi)) dt.allGateC) (ℓ : Fin (dt.nIn vi)) : dt.igPassP RF zero one vi stV ℓ

The branch's guard delivers the pass: with both flags set after the inner gates' thread, every quantified level passed its gate – what unlocks the round's semantic pack.

noncomputable def DescriptiveComplexity.Draw.Data.roundCtl {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)) (hord : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] {zero one : A} (hzo : zero ≠ one) (vi : dt.VarIx) (stV : TapeStD dt A R P) (v : Univ A R P dt.KIx dt.dd → Prop) (sem : (∀ (ℓ : Fin (dt.nIn vi)), dt.igPassP RF zero one vi stV ℓ) → (a : Fin (dt.natOf vi)) → dt.KindSem zero one vi stV (dt.kindOf vi a)) (f₀ : dt.CtlIx → A) : dt.CtlIx → A

The control one round leaves at the fold checkpoint: the matrix thread applied to the inner gates' output at a passing round – both flags set, the round's conditional semantic pack unlocked by DescriptiveComplexity.Draw.Data.roundPass_of_flags – and the gates' output alone at a skipping one. The pack must be conditional: a garbage round holds no encodings to build one from, and its matrix never runs.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.Draw.Data.roundEndSt {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.IsRelational] [L.Structure A] (zero one : A) (vi : dt.VarIx) (stV : TapeStD dt A R P) (v : Univ A R P dt.KIx dt.dd → Prop) (f₀ : dt.CtlIx → A) : TapeStD dt A R P

The state one round leaves: the matrix runs on the passing branch only, so the round's exit state is the matrix's threaded state there and the entry state at a skipping round.

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.Draw.Data.roundEndSt_fields {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.IsRelational] [L.Structure A] {zero one : A} (vi : dt.VarIx) (stV : TapeStD dt A R P) (v : Univ A R P dt.KIx dt.dd → Prop) (f₀ : dt.CtlIx → A) : (dt.roundEndSt RF zero one vi stV v f₀).wk = stV.wk ∧ (dt.roundEndSt RF zero one vi stV v f₀).mir = stV.mir ∧ (dt.roundEndSt RF zero one vi stV v f₀).bot = stV.bot ∧ (dt.roundEndSt RF zero one vi stV v f₀).val = stV.val ∧ (dt.roundEndSt RF zero one vi stV v f₀).old = stV.old

A round's exit state differs from its entry in SAV and TARGET alone – the same fact as DescriptiveComplexity.Draw.Data.matSt_fields, through the branch.

theorem DescriptiveComplexity.Draw.Data.roundEndSt_eq {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.IsRelational] [L.Structure A] {zero one : A} (vi : dt.VarIx) (stV : TapeStD dt A R P) (v : Univ A R P dt.KIx dt.dd → Prop) (f₀ : dt.CtlIx → A) : dt.roundEndSt RF zero one vi stV v f₀ = { mir := stV.mir, tgt := (dt.roundEndSt RF zero one vi stV v f₀).tgt, sav := (dt.roundEndSt RF zero one vi stV v f₀).sav, val := stV.val, old := stV.old, new := stV.new, wk := stV.wk, bot := stV.bot, ltp := stV.ltp }

A round's exit state is its entry state with the two scratch registers rewritten – the sharpening of DescriptiveComplexity.Draw.Data.roundEndSt_fields, and what lets the VAL loop thread those two registers rather than the whole state.

theorem DescriptiveComplexity.Draw.Data.scratchEq_roundEndSt {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.IsRelational] [L.Structure A] {zero one : A} (vi : dt.VarIx) (stV : TapeStD dt A R P) (v : Univ A R P dt.KIx dt.dd → Prop) (f₀ : dt.CtlIx → A) : dt.ScratchEq (dt.roundEndSt RF zero one vi stV v f₀) stV

A round's exit state differs from its entry state in the two scratch registers alone – roundEndSt_eq in the form the congruences take.

noncomputable def DescriptiveComplexity.Draw.Data.roundCtlT {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)) (hord : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] {zero one : A} (hzo : zero ≠ one) (vi : dt.VarIx) (stV : TapeStD dt A R P) (v : Univ A R P dt.KIx dt.dd → Prop) (sem : (∀ (ℓ : Fin (dt.nIn vi)), dt.igPassP RF zero one vi stV ℓ) → (a : Fin (dt.natOf vi)) → dt.KindSem zero one vi (dt.matSt vi stV v ↑a) (dt.kindOf vi a)) (f₀ : dt.CtlIx → A) : dt.CtlIx → A

The control one round leaves, threaded: as DescriptiveComplexity.Draw.Data.roundCtl, with the matrix's thread taken at the states its atoms run at.

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.Draw.Data.roundCtl_congr_scratch {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)) (hord : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] {zero one : A} (hzo : zero ≠ one) {v : Univ A R P dt.KIx dt.dd → Prop} {stV stV' : TapeStD dt A R P} (h : dt.ScratchEq stV stV') (hreg : ¬∃ (u : Univ A R P dt.KIx dt.dd), v = RF.cell u) (vi : dt.VarIx) (sem : (∀ (ℓ : Fin (dt.nIn vi)), dt.igPassP RF zero one vi stV ℓ) → (a : Fin (dt.natOf vi)) → dt.KindSem zero one vi stV (dt.kindOf vi a)) (f₀ : dt.CtlIx → A) : dt.roundCtl RF hord hzo vi stV v sem f₀ = dt.roundCtl RF hord hzo vi stV' v (fun (hp : ∀ (ℓ : Fin (dt.nIn vi)), dt.igPassP RF zero one vi stV' ℓ) (a : Fin (dt.natOf vi)) => dt.kindSemCast zero one vi ⋯ ⋯ (dt.kindOf vi a) (sem ⋯ a)) f₀

A round is blind to the two scratch registers: its gates by igFs_congr_scratch, its matrix by matFs_congr_scratch.

theorem DescriptiveComplexity.Draw.Data.roundCtlT_eq_roundCtl {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)) (hord : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] {zero one : A} (hzo : zero ≠ one) {v : Univ A R P dt.KIx dt.dd → Prop} (hreg : ¬∃ (u : Univ A R P dt.KIx dt.dd), v = RF.cell u) (vi : dt.VarIx) (stV : TapeStD dt A R P) (sem : (∀ (ℓ : Fin (dt.nIn vi)), dt.igPassP RF zero one vi stV ℓ) → (a : Fin (dt.natOf vi)) → dt.KindSem zero one vi (dt.matSt vi stV v ↑a) (dt.kindOf vi a)) (f₀ : dt.CtlIx → A) : dt.roundCtlT RF hord hzo vi stV v sem f₀ = dt.roundCtl RF hord hzo vi stV v (fun (hp : ∀ (ℓ : Fin (dt.nIn vi)), dt.igPassP RF zero one vi stV ℓ) (a : Fin (dt.natOf vi)) => dt.kindSemCast zero one vi ⋯ ⋯ (dt.kindOf vi a) (sem hp a)) f₀

The threaded round is the unthreaded one: the gates decide the branch off the same registers, and on the passing branch the matrix threads SAV and TARGET alone (matFsT_eq_matFs). With this the control the run produces is the control the semantic capstone (DescriptiveComplexity.Draw.Data.accVerdict_leafP) is stated at.

theorem DescriptiveComplexity.Draw.Data.roundCtl_apply_accC {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)) (hord : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] {zero one : A} {hzo : zero ≠ one} (vi : dt.VarIx) (stV : TapeStD dt A R P) (v : Univ A R P dt.KIx dt.dd → Prop) (sem : (∀ (ℓ : Fin (dt.nIn vi)), dt.igPassP RF zero one vi stV ℓ) → (a : Fin (dt.natOf vi)) → dt.KindSem zero one vi stV (dt.kindOf vi a)) (f₀ : dt.CtlIx → A) (jj : Fin dt.naDim) : dt.roundCtl RF hord hzo vi stV v sem f₀ (dt.accC jj) = f₀ (dt.accC jj)

The accumulators survive one whole round.

theorem DescriptiveComplexity.Draw.Data.roundCtl_apply_roundFlag {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)) (hord : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] {zero one : A} {q : dt.CtlIx} (hq : q = dt.existGateC ∨ q = dt.allGateC) {hzo : zero ≠ one} (vi : dt.VarIx) (stV : TapeStD dt A R P) (v : Univ A R P dt.KIx dt.dd → Prop) (sem : (∀ (ℓ : Fin (dt.nIn vi)), dt.igPassP RF zero one vi stV ℓ) → (a : Fin (dt.natOf vi)) → dt.KindSem zero one vi stV (dt.kindOf vi a)) (f₀ : dt.CtlIx → A) : dt.roundCtl RF hord hzo vi stV v sem f₀ q = dt.igFs RF zero one vi stV v f₀ (dt.nIn vi) q

A round's exit reads the two flags off the inner gates' thread: the matrix – run or skipped – never writes them.

theorem DescriptiveComplexity.Draw.Data.roundCtl_of_flags {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)) (hord : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] {zero one : A} {hzo : zero ≠ one} (vi : dt.VarIx) (stV : TapeStD dt A R P) (v : Univ A R P dt.KIx dt.dd → Prop) (sem : (∀ (ℓ : Fin (dt.nIn vi)), dt.igPassP RF zero one vi stV ℓ) → (a : Fin (dt.natOf vi)) → dt.KindSem zero one vi stV (dt.kindOf vi a)) (f₀ : dt.CtlIx → A) (hp : ∀ (ℓ : Fin (dt.nIn vi)), dt.igPassP RF zero one vi stV ℓ) (hEx : dt.ctlBit one (dt.igFs RF zero one vi stV v f₀ (dt.nIn vi)) dt.existGateC) (hAl : dt.ctlBit one (dt.igFs RF zero one vi stV v f₀ (dt.nIn vi)) dt.allGateC) : dt.roundCtl RF hord hzo vi stV v sem f₀ = dt.matFs RF hord zero one vi stV v (dt.varArgsOf zero one vi).enterAtomSt (sem hp) (dt.igFs RF zero one vi stV v f₀ (dt.nIn vi)) (dt.natOf vi)

A passing round's exit is the matrix thread, at any proof of the pass – the branch's own derivation is proof-irrelevant.

The inner gates' run

theorem DescriptiveComplexity.Draw.Data.igs_run {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] [Finite R] [Finite P] {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) {stV : TapeStD dt A R P} {emb : dt.IGatesPh vi → P} {exitPh : P} {rEmb : (i : dt.IGatesSite vi) → dt.IGatesSh vi i → R} [Finite dt.KIx] (hrules : ∀ (i : dt.IGatesSite vi) (ρ : dt.IGatesSh vi i), PR.rules (rEmb i ρ) = dt.igatesRule PR.one vi emb (dt.varArgsOf PR.zero PR.one vi).argsIG (dt.varArgsOf PR.zero PR.one vi).wellIGOf (dt.varArgsOf PR.zero PR.one vi).setFailIGOf (dt.varArgsOf PR.zero PR.one vi).enterIGSt exitPh i ρ) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) {gtop gbot : Univ A R P dt.KIx dt.dd} (htop : ∀ (y : Univ A R P dt.KIx dt.dd), WMLe y gtop) (hbot : ∀ (y : Univ A R P dt.KIx dt.dd), WMLe gbot y) {v v' : Univ A R P dt.KIx dt.dd → Prop} (hv : WMSetLt WMLe v (RF.cell gbot)) (hvi : WMIncr WMLe v v') (hwkSt : stV.wk = fun (r : Univ A R P dt.KIx dt.dd → Prop) => r = v) (f₀ : dt.CtlIx → A) : Relation.ReflTransGen (wideData (Univ A R P dt.KIx dt.dd)).Step { state := Sum.inr (PR.stElt (emb (SeqPh.chk 0)) f₀), head := Sum.inl v, tape := wideTape (PR.trackTapeAt RF.cell Slot.val (dt.back RF.cell PR.zero PR.one ⋯ stV) stV.val) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt exitPh (dt.igFs RF PR.zero PR.one vi stV v f₀ (dt.nIn vi))), head := Sum.inl v', tape := wideTape (PR.trackTapeAt RF.cell Slot.val (dt.back RF.cell PR.zero PR.one ⋯ stV) stV.val) (PR.syElt PR.blank) }

The inner gates' run: from the checkpoint before the first level at the marker, through every level – the file test, and either the dispatch, domain loop and conjoining exit, or the continuing fail – to the round's branch checkpoint one cell to the marker's right, the two flags spelled by the thread.

The whole round, at the program's own rules

theorem DescriptiveComplexity.Draw.Data.round_run {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] [Finite R] [Finite P] {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) {v : Univ A R P dt.KIx dt.dd → Prop} {emb : dt.VarPhF vi → P} {exitPh : P} {rEmb : (i : dt.VarSiteF vi) → dt.VarShF vi i → R} [Finite dt.KIx] (hrules : ∀ (i : dt.VarSiteF vi) (ρ : dt.VarShF vi i), PR.rules (rEmb i ρ) = dt.varRuleF PR.zero PR.one vi (dt.varArgsOf PR.zero PR.one vi) emb exitPh i ρ) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) {gtop gbot : Univ A R P dt.KIx dt.dd} (htop : ∀ (y : Univ A R P dt.KIx dt.dd), WMLe y gtop) (hbot : ∀ (y : Univ A R P dt.KIx dt.dd), WMLe gbot y) (hwork : ∀ {r : Univ A R P dt.KIx dt.dd → Prop}, ¬r gbot → ∀ (u : Univ A R P dt.KIx dt.dd), WMSetLt WMLe r (RF.cell u)) {v' : Univ A R P dt.KIx dt.dd → Prop} (hv : WMSetLt WMLe v (RF.cell gbot)) (hvi : WMIncr WMLe v v') (stV : TapeStD dt A R P) (hwkV : stV.wk = fun (r : Univ A R P dt.KIx dt.dd → Prop) => r = v) (hmirV : stV.mir = v) (hbotV : stV.bot = fun (r : Univ A R P dt.KIx dt.dd → Prop) => r = fun (x : Univ A R P dt.KIx dt.dd) => False) (hsavV : stV.sav = v) (htgtV : stV.tgt = v) (sem : (∀ (ℓ : Fin (dt.nIn vi)), dt.igPassP RF PR.zero PR.one vi stV ℓ) → (a : Fin (dt.natOf vi)) → dt.KindSem PR.zero PR.one vi stV (dt.kindOf vi a)) (f : dt.CtlIx → A) : Relation.ReflTransGen (wideData (Univ A R P dt.KIx dt.dd)).Step { state := Sum.inr (PR.stElt (emb (VarPh.matrixP (RoundPh.igP (SeqPh.chk 0)))) f), head := Sum.inl v', tape := wideTape (PR.trackTapeAt RF.cell Slot.val (dt.back RF.cell PR.zero PR.one ⋯ stV) stV.val) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (emb VarPh.mchk1) (dt.roundCtl RF hord ⋯ vi stV v sem f)), head := Sum.inl v, tape := wideTape (PR.trackTapeAt RF.cell Slot.val (dt.back RF.cell PR.zero PR.one ⋯ stV) stV.val) (PR.syElt PR.blank) }

One round of the VAL loop, run: from the dispatch's landing one cell right of the marker at the inner gates' first checkpoint, the walk-back, every quantified level's gate – pass or fail, the fail continuing – the branch checkpoint on the two flags, the matrix pass on the passing branch, and the walk-back at the fold checkpoint. No semantic hypothesis: the levels' outcomes and the branch are decided classically, so the round runs at every VAL content the loop enumerates.

theorem DescriptiveComplexity.Draw.Data.round_run_thread {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] [Finite R] [Finite P] {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) {v : Univ A R P dt.KIx dt.dd → Prop} {emb : dt.VarPhF vi → P} {exitPh : P} {rEmb : (i : dt.VarSiteF vi) → dt.VarShF vi i → R} [Finite dt.KIx] (hrules : ∀ (i : dt.VarSiteF vi) (ρ : dt.VarShF vi i), PR.rules (rEmb i ρ) = dt.varRuleF PR.zero PR.one vi (dt.varArgsOf PR.zero PR.one vi) emb exitPh i ρ) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) {gtop gbot : Univ A R P dt.KIx dt.dd} (htop : ∀ (y : Univ A R P dt.KIx dt.dd), WMLe y gtop) (hbot : ∀ (y : Univ A R P dt.KIx dt.dd), WMLe gbot y) (hwork : ∀ {r : Univ A R P dt.KIx dt.dd → Prop}, ¬r gbot → ∀ (u : Univ A R P dt.KIx dt.dd), WMSetLt WMLe r (RF.cell u)) {v' : Univ A R P dt.KIx dt.dd → Prop} (hv : WMSetLt WMLe v (RF.cell gbot)) (hvi : WMIncr WMLe v v') (stV : TapeStD dt A R P) (hwkV : stV.wk = fun (r : Univ A R P dt.KIx dt.dd → Prop) => r = v) (hmirV : stV.mir = v) (hbotV : stV.bot = fun (r : Univ A R P dt.KIx dt.dd → Prop) => r = fun (x : Univ A R P dt.KIx dt.dd) => False) (sem : (∀ (ℓ : Fin (dt.nIn vi)), dt.igPassP RF PR.zero PR.one vi stV ℓ) → (a : Fin (dt.natOf vi)) → dt.KindSem PR.zero PR.one vi (dt.matSt vi stV v ↑a) (dt.kindOf vi a)) (f : dt.CtlIx → A) : Relation.ReflTransGen (wideData (Univ A R P dt.KIx dt.dd)).Step { state := Sum.inr (PR.stElt (emb (VarPh.matrixP (RoundPh.igP (SeqPh.chk 0)))) f), head := Sum.inl v', tape := wideTape (PR.trackTapeAt RF.cell Slot.val (dt.back RF.cell PR.zero PR.one ⋯ stV) stV.val) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (emb VarPh.mchk1) (dt.roundCtlT RF hord ⋯ vi stV v sem f)), head := Sum.inl v, tape := wideTape (PR.trackTapeAt RF.cell Slot.val (dt.back RF.cell PR.zero PR.one ⋯ (dt.roundEndSt RF PR.zero PR.one vi stV v f)) (dt.roundEndSt RF PR.zero PR.one vi stV v f).val) (PR.syElt PR.blank) }

One round of the VAL loop, run – threaded: as DescriptiveComplexity.Draw.Data.round_run with no boundary discipline assumed, so it applies at every address of the outer sweep. The tape ends in DescriptiveComplexity.Draw.Data.roundEndSt, which is the entry state unless the round's matrix ran and contained a stage atom.