One round of a variable's loop at an arbitrary file

DescriptiveComplexity.Problems.Wide.DrawInstRound read at a coarse file: the inner gates of a round (their file tests, their families and their flags), the control the round folds and the round's two runs. Everything below it is already at the file, so this is the last layer before the variable's loop.

One inner gate block, in the sequencer's shape

theorem DescriptiveComplexity.Draw.Data.ixIGateBlock_reachesIn_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} {I : Type} [Finite I] (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} (hinj : Function.Injective elt) (hhasP : F.toLayout.HasName PR.zero) (heltP : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhasP b c) = dt.blkElt b (pad PR.zero c)) (hsepP : F.toLayout.NameSep PR.zero ⋯) (hix : IsLinOrd F.le) [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 : I} (htop : ∀ (y : I), F.le y gtop) (hbot : ∀ (y : I), F.le gbot y) {v v' : Univ A R P dt.KIx dt.dd → Prop} (hv : WMSetLt WMLe v (F.cell gbot)) (hvi : WMIncr WMLe v v') {st : TapeSt dt A R P I} (hwkSt : st.wk = fun (r : Univ A R P dt.KIx dt.dd → Prop) => r = v) (Test : I → Prop) {wG : ℕ} (hgap : ∀ (u u' : I), IxSucc F.le u u' → wideRank (F.cell u') - wideRank (F.cell u) ≤ wG) (hcompat : ∀ (u : I), wellG (PR.passTracksAt F.cell Slot.mir (dt.ixBack F.toLayout PR.zero PR.one ⋯ st) st.mir (F.cell u)) ↔ Test u) (w : ℕ) (hcostR : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), 2 * (wideRank (F.cell (F.toLayout.reg hhasP b c)) - wideRank v) + 2 ≤ w) (hTest : ∀ (u : I), Test u) (f : dt.CtlIx → A) : (wideData (Univ A R P dt.KIx dt.dd)).ReachesIn (wideRank (F.cell gtop) + 2 + ((ixRank F.le gtop - ixRank F.le gbot) * wG + 1) + wideRank (F.cell gbot) + (1 + (1 + ((w + 2) * Fintype.card dt.X.Tag + 2 + ((2 + (w + 2) * dt.domNr (dt.dspTagOf PR.zero PR.one (wmBlk (ixAddr elt st.val) (Tag.arg (toLex b))))) * (Nat.card (Lex (Fin dt.eDim → A)) + 1) + 1))))) { state := Sum.inr (PR.stElt (emb (Sum.inl TestPh.up)) f), head := Sum.inl v', tape := wideTape (PR.trackTapeAt F.cell Slot.val (dt.ixBack F.toLayout 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 (ixAddr elt st.val) (Tag.arg (toLex b)))) (dt.ixIGateFam F hhasP PR.one b st (dt.dspTagOf PR.zero PR.one (wmBlk (ixAddr elt st.val) (Tag.arg (toLex b)))) flag hc hn hrd v (dt.ixIGateTagFam F hhasP 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 (ixAddr elt st.val) (Tag.arg (toLex b))))))) (dt.ixBack F.toLayout PR.zero PR.one ⋯ st v))), head := Sum.inl v', tape := wideTape (PR.trackTapeAt F.cell Slot.val (dt.ixBack F.toLayout 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.ixIGateBlock_reachesIn_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} {I : Type} [Finite I] (F : LaidFile dt A R P I) (hix : IsLinOrd F.le) [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 : I} (htop : ∀ (y : I), F.le y gtop) (hbot : ∀ (y : I), F.le gbot y) {v v' : Univ A R P dt.KIx dt.dd → Prop} (hv : WMSetLt WMLe v (F.cell gbot)) (hvi : WMIncr WMLe v v') {st : TapeSt dt A R P I} (hwkSt : st.wk = fun (r : Univ A R P dt.KIx dt.dd → Prop) => r = v) (Test : I → Prop) {wG : ℕ} (hgap : ∀ (u u' : I), IxSucc F.le u u' → wideRank (F.cell u') - wideRank (F.cell u) ≤ wG) (hcompat : ∀ (u : I), wellG (PR.passTracksAt F.cell Slot.mir (dt.ixBack F.toLayout PR.zero PR.one ⋯ st) st.mir (F.cell u)) ↔ Test u) {u : I} (hTest : ¬Test u) (f : dt.CtlIx → A) : (wideData (Univ A R P dt.KIx dt.dd)).ReachesIn (wideRank (F.cell gtop) + 2 + ((ixRank F.le gtop - ixRank F.le gbot) * wG + 1) + wideRank (F.cell gbot) + 1) { state := Sum.inr (PR.stElt (emb (Sum.inl TestPh.up)) f), head := Sum.inl v', tape := wideTape (PR.trackTapeAt F.cell Slot.val (dt.ixBack F.toLayout PR.zero PR.one ⋯ st) st.val) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt failPh (setFail f (dt.ixBack F.toLayout PR.zero PR.one ⋯ st v))), head := Sum.inl v', tape := wideTape (PR.trackTapeAt F.cell Slot.val (dt.ixBack F.toLayout 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

noncomputable def DescriptiveComplexity.Draw.Data.ixIGTest {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)] {I : Type} (F : LaidFile dt A R P I) (zero one : A) (stV : TapeSt dt A R P I) (b : Fin dt.ko ⊕ Fin dt.ki) (u : I) : 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.ixIGTest F zero one stV b u = dt.wellShapedIG zero one b (dt.ixBack F.toLayout zero one ⋯ stV (F.cell u))

theorem DescriptiveComplexity.Draw.Data.ixIGTest_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)] {I : Type} (F : LaidFile dt A R P I) (zero one : A) {st st' : TapeSt dt A R P I} (hval : st.val = st'.val) (b : Fin dt.ko ⊕ Fin dt.ki) (u : I) : dt.ixIGTest F zero one st b u ↔ dt.ixIGTest F 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.ixIGFs {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.IsRelational] [L.Structure A] (zero one : A) (hhas : F.toLayout.HasName zero) (vi : dt.VarIx) (stV : TapeSt dt A R P I) (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.ixIGFs F zero one hhas vi stV v f₀ 0 = f₀

theorem DescriptiveComplexity.Draw.Data.ixIGFs_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] {I : Type} (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} [Nonempty A] [L.IsRelational] [L.Structure A] (zero one : A) (hhas : F.toLayout.HasName zero) {v : Univ A R P dt.KIx dt.dd → Prop} {stV stV' : TapeSt dt A R P I} (h : dt.ScratchEq stV stV') (hreg : ¬∃ (u : I), v = F.cell u) (vi : dt.VarIx) (f₀ : dt.CtlIx → A) (n : ℕ) : dt.ixIGFs F zero one hhas vi stV v f₀ n = dt.ixIGFs F zero one hhas 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.ixIGPassP {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) (vi : dt.VarIx) (stV : TapeSt dt A R P I) (ℓ : 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.ixIGPassP_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] {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) (vi : dt.VarIx) {st st' : TapeSt dt A R P I} (hval : st.val = st'.val) (ℓ : Fin (dt.nIn vi)) : dt.ixIGPassP F zero one vi st ℓ ↔ dt.ixIGPassP F 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.ixIGFs_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] {I : Type} (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} [Nonempty A] [L.IsRelational] [L.Structure A] {zero one : A} (hhas : F.toLayout.HasName zero) (vi : dt.VarIx) (stV : TapeSt dt A R P I) (v : Univ A R P dt.KIx dt.dd → Prop) (f₀ : dt.CtlIx → A) (jj : Fin dt.naDim) (n : ℕ) : dt.ixIGFs F zero one hhas 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.ixKindExitCtl_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] {I : Type} (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} [Nonempty A] [L.IsRelational] [L.Structure A] {zero one : A} (hhas : F.toLayout.HasName zero) {q : dt.CtlIx} (hq : q = dt.existGateC ∨ q = dt.allGateC) (vi : dt.VarIx) (av : Fin dt.natMax) (st : TapeSt dt A R P I) (v : Univ A R P dt.KIx dt.dd → Prop) (κ : MatAtom dt.X dt.d.B (dt.nOf vi)) (sem : dt.IxKindSem zero one vi st elt κ) (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.ixKindExitCtl F zero one hhas 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.ixMatFs_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] {I : Type} (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} [Nonempty A] [L.IsRelational] [L.Structure A] {zero one : A} (hhas : F.toLayout.HasName zero) {q : dt.CtlIx} (hq : q = dt.existGateC ∨ q = dt.allGateC) (vi : dt.VarIx) (st : TapeSt dt A R P I) (v : Univ A R P dt.KIx dt.dd → Prop) (sem : (b : Fin (dt.natOf vi)) → dt.IxKindSem zero one vi st elt (dt.kindOf vi b)) (f₀ : dt.CtlIx → A) (n : ℕ) : dt.ixMatFs F zero one hhas 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_ixIGFs_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] {I : Type} (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} (hinj : Function.Injective elt) [Nonempty A] [L.IsRelational] [L.Structure A] {zero one : A} (hhas : F.toLayout.HasName zero) (helt : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhas b c) = dt.blkElt b (pad zero c)) (hzo : zero ≠ one) {q : dt.CtlIx} (hq : q = dt.existGateC ∨ q = dt.allGateC) (vi : dt.VarIx) (stV : TapeSt dt A R P I) (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.ixIGFs F zero one hhas vi stV v f₀ (n + 1)) q ↔ dt.ctlBit one ((dt.varArgsOf zero one vi).enterIGSt ⟨n, hℓn⟩ (dt.ixIGFs F zero one hhas vi stV v f₀ n) (dt.ixBack F.toLayout zero one ⋯ stV v)) q ∧ (dt.igFlag vi ⟨n, hℓn⟩ = q → dt.ixIGPassP F 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_ixIGFs {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} (hinj : Function.Injective elt) [Nonempty A] [L.IsRelational] [L.Structure A] {zero one : A} (hhas : F.toLayout.HasName zero) (helt : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhas b c) = dt.blkElt b (pad zero c)) (hzo : zero ≠ one) {q : dt.CtlIx} (hq : q = dt.existGateC ∨ q = dt.allGateC) (vi : dt.VarIx) (stV : TapeSt dt A R P I) (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.ixIGFs F zero one hhas vi stV v f₀ n) q ↔ ∀ (ℓ : Fin (dt.nIn vi)), ↑ℓ < n → dt.igFlag vi ℓ = q → dt.ixIGPassP F 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.ixRoundPass_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] {I : Type} (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} (hinj : Function.Injective elt) [Nonempty A] [L.IsRelational] [L.Structure A] {zero one : A} (hhas : F.toLayout.HasName zero) (helt : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhas b c) = dt.blkElt b (pad zero c)) (hzo : zero ≠ one) (vi : dt.VarIx) (stV : TapeSt dt A R P I) (v : Univ A R P dt.KIx dt.dd → Prop) (f₀ : dt.CtlIx → A) (h : dt.ctlBit one (dt.ixIGFs F zero one hhas vi stV v f₀ (dt.nIn vi)) dt.existGateC ∧ dt.ctlBit one (dt.ixIGFs F zero one hhas vi stV v f₀ (dt.nIn vi)) dt.allGateC) (ℓ : Fin (dt.nIn vi)) : dt.ixIGPassP F 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.ixRoundCtl {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} (hinj : Function.Injective elt) [Nonempty A] [L.IsRelational] [L.Structure A] {zero one : A} (hhas : F.toLayout.HasName zero) (helt : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhas b c) = dt.blkElt b (pad zero c)) (hzo : zero ≠ one) (vi : dt.VarIx) (stV : TapeSt dt A R P I) (v : Univ A R P dt.KIx dt.dd → Prop) (sem : (∀ (ℓ : Fin (dt.nIn vi)), dt.ixIGPassP F zero one vi stV ℓ) → (a : Fin (dt.natOf vi)) → dt.IxKindSem zero one vi stV elt (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.ixRoundEndSt {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.IsRelational] [L.Structure A] (zero one : A) (hhas : F.toLayout.HasName zero) (vi : dt.VarIx) (stV : TapeSt dt A R P I) (v : Univ A R P dt.KIx dt.dd → Prop) (f₀ : dt.CtlIx → A) : TapeSt dt A R P I

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.ixRoundEndSt_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] {I : Type} (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} [Nonempty A] [L.IsRelational] [L.Structure A] {zero one : A} (hhas : F.toLayout.HasName zero) (vi : dt.VarIx) (stV : TapeSt dt A R P I) (v : Univ A R P dt.KIx dt.dd → Prop) (f₀ : dt.CtlIx → A) : (dt.ixRoundEndSt F zero one hhas vi stV v f₀).wk = stV.wk ∧ (dt.ixRoundEndSt F zero one hhas vi stV v f₀).mir = stV.mir ∧ (dt.ixRoundEndSt F zero one hhas vi stV v f₀).bot = stV.bot ∧ (dt.ixRoundEndSt F zero one hhas vi stV v f₀).val = stV.val ∧ (dt.ixRoundEndSt F zero one hhas 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.ixRoundEndSt_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] {I : Type} (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} [Nonempty A] [L.IsRelational] [L.Structure A] {zero one : A} (hhas : F.toLayout.HasName zero) (vi : dt.VarIx) (stV : TapeSt dt A R P I) (v : Univ A R P dt.KIx dt.dd → Prop) (f₀ : dt.CtlIx → A) : dt.ixRoundEndSt F zero one hhas vi stV v f₀ = { mir := stV.mir, tgt := (dt.ixRoundEndSt F zero one hhas vi stV v f₀).tgt, sav := (dt.ixRoundEndSt F zero one hhas 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.ixScratchEq_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] {I : Type} (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} [Nonempty A] [L.IsRelational] [L.Structure A] {zero one : A} (hhas : F.toLayout.HasName zero) (vi : dt.VarIx) (stV : TapeSt dt A R P I) (v : Univ A R P dt.KIx dt.dd → Prop) (f₀ : dt.CtlIx → A) : dt.ScratchEq (dt.ixRoundEndSt F zero one hhas 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.ixRoundCtlT {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} (hinj : Function.Injective elt) [Nonempty A] [L.IsRelational] [L.Structure A] {zero one : A} (hhas : F.toLayout.HasName zero) (helt : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhas b c) = dt.blkElt b (pad zero c)) (hzo : zero ≠ one) (vi : dt.VarIx) (stV : TapeSt dt A R P I) (v : Univ A R P dt.KIx dt.dd → Prop) (sem : (∀ (ℓ : Fin (dt.nIn vi)), dt.ixIGPassP F zero one vi stV ℓ) → (a : Fin (dt.natOf vi)) → dt.IxKindSem zero one vi (dt.ixMatSt vi stV v ↑a) elt (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.ixRoundCtl_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] {I : Type} (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} (hinj : Function.Injective elt) [Nonempty A] [L.IsRelational] [L.Structure A] {zero one : A} (hhas : F.toLayout.HasName zero) (helt : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhas b c) = dt.blkElt b (pad zero c)) (hzo : zero ≠ one) {v : Univ A R P dt.KIx dt.dd → Prop} {stV stV' : TapeSt dt A R P I} (h : dt.ScratchEq stV stV') (hreg : ¬∃ (u : I), v = F.cell u) (vi : dt.VarIx) (sem : (∀ (ℓ : Fin (dt.nIn vi)), dt.ixIGPassP F zero one vi stV ℓ) → (a : Fin (dt.natOf vi)) → dt.IxKindSem zero one vi stV elt (dt.kindOf vi a)) (f₀ : dt.CtlIx → A) : dt.ixRoundCtl F hinj hhas helt hzo vi stV v sem f₀ = dt.ixRoundCtl F hinj hhas helt hzo vi stV' v (fun (hp : ∀ (ℓ : Fin (dt.nIn vi)), dt.ixIGPassP F zero one vi stV' ℓ) (a : Fin (dt.natOf vi)) => dt.ixKindSemCast 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.ixRoundCtlT_eq_ixRoundCtl {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} (hinj : Function.Injective elt) [Nonempty A] [L.IsRelational] [L.Structure A] {zero one : A} (hhas : F.toLayout.HasName zero) (helt : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhas b c) = dt.blkElt b (pad zero c)) (hzo : zero ≠ one) {v : Univ A R P dt.KIx dt.dd → Prop} (hreg : ¬∃ (u : I), v = F.cell u) (vi : dt.VarIx) (stV : TapeSt dt A R P I) (sem : (∀ (ℓ : Fin (dt.nIn vi)), dt.ixIGPassP F zero one vi stV ℓ) → (a : Fin (dt.natOf vi)) → dt.IxKindSem zero one vi (dt.ixMatSt vi stV v ↑a) elt (dt.kindOf vi a)) (f₀ : dt.CtlIx → A) : dt.ixRoundCtlT F hinj hhas helt hzo vi stV v sem f₀ = dt.ixRoundCtl F hinj hhas helt hzo vi stV v (fun (hp : ∀ (ℓ : Fin (dt.nIn vi)), dt.ixIGPassP F zero one vi stV ℓ) (a : Fin (dt.natOf vi)) => dt.ixKindSemCast 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.ixRoundCtl_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] {I : Type} (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} (hinj : Function.Injective elt) [Nonempty A] [L.IsRelational] [L.Structure A] {zero one : A} (hhas : F.toLayout.HasName zero) (helt : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhas b c) = dt.blkElt b (pad zero c)) {hzo : zero ≠ one} (vi : dt.VarIx) (stV : TapeSt dt A R P I) (v : Univ A R P dt.KIx dt.dd → Prop) (sem : (∀ (ℓ : Fin (dt.nIn vi)), dt.ixIGPassP F zero one vi stV ℓ) → (a : Fin (dt.natOf vi)) → dt.IxKindSem zero one vi stV elt (dt.kindOf vi a)) (f₀ : dt.CtlIx → A) (jj : Fin dt.naDim) : dt.ixRoundCtl F hinj hhas helt hzo vi stV v sem f₀ (dt.accC jj) = f₀ (dt.accC jj)

The accumulators survive one whole round.

theorem DescriptiveComplexity.Draw.Data.ixRoundCtl_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] {I : Type} (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} (hinj : Function.Injective elt) [Nonempty A] [L.IsRelational] [L.Structure A] {zero one : A} (hhas : F.toLayout.HasName zero) (helt : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhas b c) = dt.blkElt b (pad zero c)) {q : dt.CtlIx} (hq : q = dt.existGateC ∨ q = dt.allGateC) {hzo : zero ≠ one} (vi : dt.VarIx) (stV : TapeSt dt A R P I) (v : Univ A R P dt.KIx dt.dd → Prop) (sem : (∀ (ℓ : Fin (dt.nIn vi)), dt.ixIGPassP F zero one vi stV ℓ) → (a : Fin (dt.natOf vi)) → dt.IxKindSem zero one vi stV elt (dt.kindOf vi a)) (f₀ : dt.CtlIx → A) : dt.ixRoundCtl F hinj hhas helt hzo vi stV v sem f₀ q = dt.ixIGFs F zero one hhas 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.ixRoundCtl_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] {I : Type} (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} (hinj : Function.Injective elt) [Nonempty A] [L.IsRelational] [L.Structure A] {zero one : A} (hhas : F.toLayout.HasName zero) (helt : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhas b c) = dt.blkElt b (pad zero c)) {hzo : zero ≠ one} (vi : dt.VarIx) (stV : TapeSt dt A R P I) (v : Univ A R P dt.KIx dt.dd → Prop) (sem : (∀ (ℓ : Fin (dt.nIn vi)), dt.ixIGPassP F zero one vi stV ℓ) → (a : Fin (dt.natOf vi)) → dt.IxKindSem zero one vi stV elt (dt.kindOf vi a)) (f₀ : dt.CtlIx → A) (hp : ∀ (ℓ : Fin (dt.nIn vi)), dt.ixIGPassP F zero one vi stV ℓ) (hEx : dt.ctlBit one (dt.ixIGFs F zero one hhas vi stV v f₀ (dt.nIn vi)) dt.existGateC) (hAl : dt.ctlBit one (dt.ixIGFs F zero one hhas vi stV v f₀ (dt.nIn vi)) dt.allGateC) : dt.ixRoundCtl F hinj hhas helt hzo vi stV v sem f₀ = dt.ixMatFs F zero one hhas vi stV v (dt.varArgsOf zero one vi).enterAtomSt (sem hp) (dt.ixIGFs F zero one hhas 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.ixIGs_reachesIn {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} {I : Type} [Finite I] (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} (hinj : Function.Injective elt) (hhasP : F.toLayout.HasName PR.zero) (heltP : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhasP b c) = dt.blkElt b (pad PR.zero c)) (hsepP : F.toLayout.NameSep PR.zero ⋯) (hix : IsLinOrd F.le) [Nonempty A] [L.IsRelational] [L.Structure A] (vi : dt.VarIx) {stV : TapeSt dt A R P I} {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 ρ) {wG : ℕ} (hgap : ∀ (u u' : I), IxSucc F.le u u' → wideRank (F.cell u') - wideRank (F.cell u) ≤ wG) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) {gtop gbot : I} (htop : ∀ (y : I), F.le y gtop) (hbot : ∀ (y : I), F.le gbot y) {v v' : Univ A R P dt.KIx dt.dd → Prop} (hv : WMSetLt WMLe v (F.cell gbot)) (hvi : WMIncr WMLe v v') (hwkSt : stV.wk = fun (r : Univ A R P dt.KIx dt.dd → Prop) => r = v) (w wP : ℕ) (hwP : wideRank (F.cell gtop) + 2 + ((ixRank F.le gtop - ixRank F.le gbot) * wG + 1) + wideRank (F.cell gbot) ≤ wP) (hcostR : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), 2 * (wideRank (F.cell (F.toLayout.reg hhasP b c)) - wideRank v) + 2 ≤ w) (f₀ : dt.CtlIx → A) : (wideData (Univ A R P dt.KIx dt.dd)).ReachesIn ((dt.ixGateCost A w wP + 2) * dt.nIn vi + 1) { state := Sum.inr (PR.stElt (emb (SeqPh.chk 0)) f₀), head := Sum.inl v, tape := wideTape (PR.trackTapeAt F.cell Slot.val (dt.ixBack F.toLayout PR.zero PR.one ⋯ stV) stV.val) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt exitPh (dt.ixIGFs F PR.zero PR.one hhasP vi stV v f₀ (dt.nIn vi))), head := Sum.inl v', tape := wideTape (PR.trackTapeAt F.cell Slot.val (dt.ixBack F.toLayout PR.zero PR.one ⋯ stV) stV.val) (PR.syElt PR.blank) }

The inner gates' run, on a clock: as DescriptiveComplexity.Draw.Data.ixIGs_run with the levels counted – one level's width, its dispatch and the step back per level, and one step to leave.

theorem DescriptiveComplexity.Draw.Data.ixIGs_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} {I : Type} [Finite I] (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} (hinj : Function.Injective elt) (hhasP : F.toLayout.HasName PR.zero) (heltP : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhasP b c) = dt.blkElt b (pad PR.zero c)) (hsepP : F.toLayout.NameSep PR.zero ⋯) (hix : IsLinOrd F.le) [Nonempty A] [L.IsRelational] [L.Structure A] (vi : dt.VarIx) {stV : TapeSt dt A R P I} {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 ρ) {wG : ℕ} (hgap : ∀ (u u' : I), IxSucc F.le u u' → wideRank (F.cell u') - wideRank (F.cell u) ≤ wG) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) {gtop gbot : I} (htop : ∀ (y : I), F.le y gtop) (hbot : ∀ (y : I), F.le gbot y) {v v' : Univ A R P dt.KIx dt.dd → Prop} (hv : WMSetLt WMLe v (F.cell gbot)) (hvi : WMIncr WMLe v v') (hwkSt : stV.wk = fun (r : Univ A R P dt.KIx dt.dd → Prop) => r = v) (w wP : ℕ) (hwP : wideRank (F.cell gtop) + 2 + ((ixRank F.le gtop - ixRank F.le gbot) * wG + 1) + wideRank (F.cell gbot) ≤ wP) (hcostR : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), 2 * (wideRank (F.cell (F.toLayout.reg hhasP b c)) - wideRank v) + 2 ≤ w) (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 F.cell Slot.val (dt.ixBack F.toLayout PR.zero PR.one ⋯ stV) stV.val) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt exitPh (dt.ixIGFs F PR.zero PR.one hhasP vi stV v f₀ (dt.nIn vi))), head := Sum.inl v', tape := wideTape (PR.trackTapeAt F.cell Slot.val (dt.ixBack F.toLayout 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

noncomputable def DescriptiveComplexity.Draw.Data.ixRoundCost {L : FirstOrder.Language} (dt : Data L) (A : Type) (vi : dt.VarIx) (w wP wR wK : ℕ) : ℕ

What one round of the VAL loop is charged: the walk-back, the inner gates, the walk-back at the branch checkpoint, the branching dispatch and its walk-back, the matrix, and the walk-back at the fold checkpoint. The skipping branch is shorter and is charged the same.

Equations

• dt.ixRoundCost A vi w wP wR wK = 1 + ((dt.ixGateCost A w wP + 2) * dt.nIn vi + 1) + 1 + 1 + 1 + ((dt.ixMatCost A vi w wP wR wK + 2) * dt.natOf vi + 1) + 1

theorem DescriptiveComplexity.Draw.Data.ixRound_reachesIn {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} {I : Type} [Finite I] (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} (hinj : Function.Injective elt) (hhasP : F.toLayout.HasName PR.zero) (heltP : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhasP b c) = dt.blkElt b (pad PR.zero c)) (hsepP : F.toLayout.NameSep PR.zero ⋯) (hix : IsLinOrd F.le) {e₀ : Univ A R P dt.KIx dt.dd} (he₀ : ∀ (y : Univ A R P dt.KIx dt.dd), WMLe e₀ y) (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 ρ) {wG : ℕ} (hgap : ∀ (u u' : I), IxSucc F.le u u' → wideRank (F.cell u') - wideRank (F.cell u) ≤ wG) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) {gtop gbot : I} (htop : ∀ (y : I), F.le y gtop) (hbot : ∀ (y : I), F.le gbot y) (hwork : ∀ {r : Univ A R P dt.KIx dt.dd → Prop}, (∀ (x : Univ A R P dt.KIx dt.dd), r x → ∃ (i : dt.KIx), x.1 = Tag.arg i) → ∀ (u : I), WMSetLt WMLe r (F.cell u)) {v' : Univ A R P dt.KIx dt.dd → Prop} (hv : WMSetLt WMLe v (F.cell gbot)) (hvi : WMIncr WMLe v v') {Use : I → Prop} (hmono : ∀ (u u' : I), WMLt F.le u u' ↔ WMLt WMLe (elt u) (elt u')) (hup : ∀ (u : I) (x : Univ A R P dt.KIx dt.dd), Use u → WMLt WMLe (elt u) x → ∃ (u' : I), Use u' ∧ elt u' = x) (hvh : IxHolds elt Use v) (hxdUse : ∀ {iv : dt.d.B.ι} (ℓ : Fin (dt.d.B.arity iv)) (b : Lex (Fin dt.dd0 → A)), Use (dt.ixStageXD F hhasP ℓ b)) (w wP wR wK : ℕ) (hwP : wideRank (F.cell gtop) + 2 + ((ixRank F.le gtop - ixRank F.le gbot) * wG + 1) + wideRank (F.cell gbot) ≤ wP) (hwR : ∀ (s : Univ A R P dt.KIx dt.dd → Prop), WMSetLt WMLe s (F.cell gbot) → wideRank s + 4 ≤ wR) (hwK : ∀ (T : Univ A R P dt.KIx dt.dd → Prop), WMSetLt WMLe T (F.cell gbot) → wideRank T * (1 + (wideRank (F.cell gtop) + 3 + (ixRank F.le gtop - ixRank F.le gbot) * wG + wideRank (F.cell gbot)) + (wideRank (F.cell gtop) + ((ixRank F.le gtop - ixRank F.le gbot) * wG + 1) + wideRank (F.cell gbot) + 4)) + 1 + (wideRank (F.cell gtop) + 3 + (ixRank F.le gtop - ixRank F.le gbot) * wG + wideRank (F.cell gbot)) ≤ wK) (hcostR : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), 2 * (wideRank (F.cell (F.toLayout.reg hhasP b c)) - wideRank v) + 2 ≤ w) (stV : TapeSt dt A R P I) (hwkV : stV.wk = fun (r : Univ A R P dt.KIx dt.dd → Prop) => r = v) (hmirV : stV.mir = ixMark elt 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 = ixMark elt v) (htgtV : stV.tgt = ixMark elt v) (sem : (∀ (ℓ : Fin (dt.nIn vi)), dt.ixIGPassP F PR.zero PR.one vi stV ℓ) → (a : Fin (dt.natOf vi)) → dt.IxKindSem PR.zero PR.one vi stV elt (dt.kindOf vi a)) (f : dt.CtlIx → A) : (wideData (Univ A R P dt.KIx dt.dd)).ReachesIn (dt.ixRoundCost A vi w wP wR wK) { state := Sum.inr (PR.stElt (emb (VarPh.matrixP (RoundPh.igP (SeqPh.chk 0)))) f), head := Sum.inl v', tape := wideTape (PR.trackTapeAt F.cell Slot.val (dt.ixBack F.toLayout PR.zero PR.one ⋯ stV) stV.val) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (emb VarPh.mchk1) (dt.ixRoundCtl F hinj hhasP heltP ⋯ vi stV v sem f)), head := Sum.inl v, tape := wideTape (PR.trackTapeAt F.cell Slot.val (dt.ixBack F.toLayout 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.ixRound_run_thread_reachesIn {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} {I : Type} [Finite I] (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} (hinj : Function.Injective elt) (hhasP : F.toLayout.HasName PR.zero) (heltP : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhasP b c) = dt.blkElt b (pad PR.zero c)) (hsepP : F.toLayout.NameSep PR.zero ⋯) (hix : IsLinOrd F.le) {e₀ : Univ A R P dt.KIx dt.dd} (he₀ : ∀ (y : Univ A R P dt.KIx dt.dd), WMLe e₀ y) (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 ρ) {wG : ℕ} (hgap : ∀ (u u' : I), IxSucc F.le u u' → wideRank (F.cell u') - wideRank (F.cell u) ≤ wG) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) {gtop gbot : I} (htop : ∀ (y : I), F.le y gtop) (hbot : ∀ (y : I), F.le gbot y) (hwork : ∀ {r : Univ A R P dt.KIx dt.dd → Prop}, (∀ (x : Univ A R P dt.KIx dt.dd), r x → ∃ (i : dt.KIx), x.1 = Tag.arg i) → ∀ (u : I), WMSetLt WMLe r (F.cell u)) {v' : Univ A R P dt.KIx dt.dd → Prop} (hv : WMSetLt WMLe v (F.cell gbot)) (hvi : WMIncr WMLe v v') {Use : I → Prop} (hmono : ∀ (u u' : I), WMLt F.le u u' ↔ WMLt WMLe (elt u) (elt u')) (hup : ∀ (u : I) (x : Univ A R P dt.KIx dt.dd), Use u → WMLt WMLe (elt u) x → ∃ (u' : I), Use u' ∧ elt u' = x) (hvh : IxHolds elt Use v) (hxdUse : ∀ {iv : dt.d.B.ι} (ℓ : Fin (dt.d.B.arity iv)) (b : Lex (Fin dt.dd0 → A)), Use (dt.ixStageXD F hhasP ℓ b)) (w wP wR wK : ℕ) (hwP : wideRank (F.cell gtop) + 2 + ((ixRank F.le gtop - ixRank F.le gbot) * wG + 1) + wideRank (F.cell gbot) ≤ wP) (hwR : ∀ (s : Univ A R P dt.KIx dt.dd → Prop), WMSetLt WMLe s (F.cell gbot) → wideRank s + 4 ≤ wR) (hwK : ∀ (T : Univ A R P dt.KIx dt.dd → Prop), WMSetLt WMLe T (F.cell gbot) → wideRank T * (1 + (wideRank (F.cell gtop) + 3 + (ixRank F.le gtop - ixRank F.le gbot) * wG + wideRank (F.cell gbot)) + (wideRank (F.cell gtop) + ((ixRank F.le gtop - ixRank F.le gbot) * wG + 1) + wideRank (F.cell gbot) + 4)) + 1 + (wideRank (F.cell gtop) + 3 + (ixRank F.le gtop - ixRank F.le gbot) * wG + wideRank (F.cell gbot)) ≤ wK) (hcostR : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), 2 * (wideRank (F.cell (F.toLayout.reg hhasP b c)) - wideRank v) + 2 ≤ w) (stV : TapeSt dt A R P I) (hwkV : stV.wk = fun (r : Univ A R P dt.KIx dt.dd → Prop) => r = v) (hmirV : stV.mir = ixMark elt 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.ixIGPassP F PR.zero PR.one vi stV ℓ) → (a : Fin (dt.natOf vi)) → dt.IxKindSem PR.zero PR.one vi (dt.ixMatSt vi stV v ↑a) elt (dt.kindOf vi a)) (f : dt.CtlIx → A) : (wideData (Univ A R P dt.KIx dt.dd)).ReachesIn (dt.ixRoundCost A vi w wP wR wK) { state := Sum.inr (PR.stElt (emb (VarPh.matrixP (RoundPh.igP (SeqPh.chk 0)))) f), head := Sum.inl v', tape := wideTape (PR.trackTapeAt F.cell Slot.val (dt.ixBack F.toLayout PR.zero PR.one ⋯ stV) stV.val) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (emb VarPh.mchk1) (dt.ixRoundCtlT F hinj hhasP heltP ⋯ vi stV v sem f)), head := Sum.inl v, tape := wideTape (PR.trackTapeAt F.cell Slot.val (dt.ixBack F.toLayout PR.zero PR.one ⋯ (dt.ixRoundEndSt F PR.zero PR.one hhasP vi stV v f)) (dt.ixRoundEndSt F PR.zero PR.one hhasP 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.