The atom kinds, dispatched: one stage interface for the matrix

The matrix's sequencer treats every classified atom alike; this file makes that literal. DescriptiveComplexity.Draw.Data.KindSem carries the one piece of semantic data a kind's run needs (the encoded points, for an expansion atom – the others need none), DescriptiveComplexity.Draw.Data.kindExitCtl is the control each kind's machinery leaves behind, and DescriptiveComplexity.Draw.Data.kind_hStage is the uniform stage discharge: whatever the kind, from the machinery's entry phase one cell right of the marker to the exit phase back there, at the Slot.val-walked presentation – the shape DescriptiveComplexity.Draw.seq_run consumes.

Generic slot-preservation through the generated families

noncomputable def DescriptiveComplexity.Draw.Data.KindSem {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [LinearOrder A] [L.Structure A] (zero one : A) (vi : dt.VarIx) (st : TapeStD dt A R P) : MatAtom dt.X dt.d.B (dt.nOf vi) → Type

The semantic data of one atom's run: an expansion atom needs the points its levels' registers encode; the other kinds need nothing.

Equations

• One or more equations did not get rendered due to their size.
• dt.KindSem zero one vi st (DescriptiveComplexity.Draw.MatAtom.eq a a_1) = PUnit.{1}
• dt.KindSem zero one vi st (DescriptiveComplexity.Draw.MatAtom.ord a a_1) = PUnit.{1}
• dt.KindSem zero one vi st (DescriptiveComplexity.Draw.MatAtom.stage i a) = PUnit.{1}

noncomputable def DescriptiveComplexity.Draw.Data.kindSemCast {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [LinearOrder A] [L.Structure A] (zero one : A) (vi : dt.VarIx) {st st' : TapeStD dt A R P} (hmir : st.mir = st'.mir) (hval : st.val = st'.val) (κ : MatAtom dt.X dt.d.B (dt.nOf vi)) (s : dt.KindSem zero one vi st κ) : dt.KindSem zero one vi st' κ

A semantic pack transports along the registers it reads. DescriptiveComplexity.Draw.Data.KindSem sees the tape state only through the levels' register sets, so a pack at one state is a pack at every state with the same mirror and VAL. This is what lets one pack – built at an address's entry state – serve every position of the spine and every round of the VAL loop, whose states differ from it in the tracks they have written and in the two scratch registers.

Equations

• dt.kindSemCast zero one vi hmir hval (DescriptiveComplexity.Draw.MatAtom.eq a a_1) s_2 = s_2
• dt.kindSemCast zero one vi hmir hval (DescriptiveComplexity.Draw.MatAtom.ord a a_1) s_2 = s_2
• dt.kindSemCast zero one vi hmir hval (DescriptiveComplexity.Draw.MatAtom.stage i a) s_2 = s_2
• dt.kindSemCast zero one vi hmir hval (DescriptiveComplexity.Draw.MatAtom.exp a ts) s_2 = ⟨↑s_2, ⋯⟩

theorem DescriptiveComplexity.Draw.Data.kindSemCast_triple {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [LinearOrder A] [L.Structure A] (zero one : A) (vi : dt.VarIx) {st₁ st₂ st₃ : TapeStD dt A R P} (h1 : st₁.mir = st₂.mir) (h2 : st₁.val = st₂.val) (h3 : st₂.mir = st₃.mir) (h4 : st₂.val = st₃.val) (h5 : st₃.mir = st₁.mir) (h6 : st₃.val = st₁.val) (κ : MatAtom dt.X dt.d.B (dt.nOf vi)) (s : dt.KindSem zero one vi st₁ κ) : dt.kindSemCast zero one vi h5 h6 κ (dt.kindSemCast zero one vi h3 h4 κ (dt.kindSemCast zero one vi h1 h2 κ s)) = s

A round trip of transports is the identity – the shape the VAL loop's bridge closes with: the pack leaves the round state, travels to the round's own state and to the state its matrix threads, and comes back.

noncomputable def DescriptiveComplexity.Draw.Data.kindExitCtl {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) (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)) : dt.KindSem zero one vi st κ → dt.kindArgs κ * Fintype.card dt.X.Tag ≤ dt.ntgDim → dt.kindDepth κ ≤ dt.eDim → dt.kindReads κ ≤ dt.nfDim → (dt.CtlIx → A) → dt.CtlIx → A

The control one atom's machinery leaves behind, by kind: the fold's exit at the comparison's or the expansion atom's family, the verdict store at the stage atom's read bit.

Equations

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

theorem DescriptiveComplexity.Draw.Data.kindExitCtl_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} {vi : dt.VarIx} {av : Fin dt.natMax} {st : TapeStD dt A R P} {v : Univ A R P dt.KIx dt.dd → Prop} {st' : TapeStD dt A R P} (h : dt.ScratchEq st st') (hreg : ¬∃ (u : Univ A R P dt.KIx dt.dd), v = RF.cell u) (κ : 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) (hn : 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 hn hrd f = dt.kindExitCtl RF hord zero one vi av st' v κ (dt.kindSemCast zero one vi ⋯ ⋯ κ sem) hk hn hrd f

An atom's machinery is blind to the two scratch registers: each kind's loop reads the levels' register sets and its background at the working cell, and each kind's exit reads the control alone (DescriptiveComplexity.Draw.Data.cmpArgs_exitSt_congr and its two siblings). The pack travels by DescriptiveComplexity.Draw.Data.kindSemCast, which keeps its points. This is the brick the whole threaded-versus-unthreaded bridge is built from.

noncomputable def DescriptiveComplexity.Draw.Data.kindEndSt {L : FirstOrder.Language} (dt : Data L) {A R P : Type} (vi : dt.VarIx) (v : Univ A R P dt.KIx dt.dd → Prop) (κ : MatAtom dt.X dt.d.B (dt.nOf vi)) (st : TapeStD dt A R P) : TapeStD dt A R P

The state an atom leaves: a stage atom normalizes SAV and TARGET to the home address (its random access writes them whatever they held), every other kind leaves the state alone.

Equations

• dt.kindEndSt vi v (DescriptiveComplexity.Draw.MatAtom.stage i a) st = DescriptiveComplexity.Draw.Data.stageEndSt st v
• dt.kindEndSt vi v κ st = st

theorem DescriptiveComplexity.Draw.Data.kind_hStage {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} {av : Fin dt.natMax} {st : TapeStD dt A R P} {v : Univ A R P dt.KIx dt.dd → Prop} [Finite dt.KIx] (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') (hwkSt : st.wk = fun (r : Univ A R P dt.KIx dt.dd → Prop) => r = v) (hmirSt : st.mir = v) (hbotSt : st.bot = fun (r : Univ A R P dt.KIx dt.dd → Prop) => r = fun (x : Univ A R P dt.KIx dt.dd) => False) (hsav : st.sav = v) (htgt : st.tgt = v) (κ : MatAtom dt.X dt.d.B (dt.nOf vi)) (hk : dt.kindArgs κ * Fintype.card dt.X.Tag ≤ dt.ntgDim) (hnd : dt.kindDepth κ ≤ dt.eDim) (hrd : dt.kindReads κ ≤ dt.nfDim) (sem : dt.KindSem PR.zero PR.one vi st κ) {emb : dt.KindPh κ → P} {exitPh : P} {rEmb : (s : dt.KindSite κ) → dt.KindSh κ s → R} (hrules : ∀ (s : dt.KindSite κ) (ρ : dt.KindSh κ s), PR.rules (rEmb s ρ) = dt.kindRule PR.zero PR.one κ (dt.kindArgsOf PR.zero PR.one vi av κ hk hnd hrd) emb exitPh s ρ) (f : dt.CtlIx → A) : Relation.ReflTransGen (wideData (Univ A R P dt.KIx dt.dd)).Step { state := Sum.inr (PR.stElt (emb (dt.kindEntry κ)) 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.kindExitCtl RF hord PR.zero PR.one vi av st v κ sem hk hnd hrd 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) }

The uniform stage discharge: whatever the kind, the atom's machinery runs from its entry phase one cell right of the marker to the exit phase back there, leaving DescriptiveComplexity.Draw.Data.kindExitCtl in the control and the tape untouched.

The matrix, assembled

noncomputable def DescriptiveComplexity.Draw.Data.matFs {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) (vi : dt.VarIx) (st : TapeStD dt A R P) (v : Univ A R P dt.KIx dt.dd → Prop) (enterSt : Fin (dt.natOf vi) → (dt.CtlIx → A) → (dt.SlotIx → A) → dt.CtlIx → A) (sem : (a : Fin (dt.natOf vi)) → dt.KindSem zero one vi st (dt.kindOf vi a)) (f₀ : dt.CtlIx → A) : ℕ → dt.CtlIx → A

The control thread across the matrix's atoms: each atom's machinery entered through the dispatch's enterSt, its exit control the next atom's input.

Equations

• One or more equations did not get rendered due to their size.
• dt.matFs RF hord zero one vi st v enterSt sem f₀ 0 = f₀

The threaded states of the matrix

noncomputable def DescriptiveComplexity.Draw.Data.matSt {L : FirstOrder.Language} (dt : Data L) {A R P : Type} (vi : dt.VarIx) (st : TapeStD dt A R P) (v : Univ A R P dt.KIx dt.dd → Prop) : ℕ → TapeStD dt A R P

The state after the matrix's first n atoms: each stage atom normalizes SAV and TARGET, the other kinds change nothing.

Equations

• dt.matSt vi st v 0 = st
• dt.matSt vi st v n.succ = if h : n < dt.natOf vi then dt.kindEndSt vi v (dt.kindOf vi ⟨n, h⟩) (dt.matSt vi st v n) else dt.matSt vi st v n

theorem DescriptiveComplexity.Draw.Data.matSt_fields {L : FirstOrder.Language} {dt : Data L} {A R P : Type} {vi : dt.VarIx} {st : TapeStD dt A R P} {v : Univ A R P dt.KIx dt.dd → Prop} (n : ℕ) : (dt.matSt vi st v n).wk = st.wk ∧ (dt.matSt vi st v n).mir = st.mir ∧ (dt.matSt vi st v n).bot = st.bot ∧ (dt.matSt vi st v n).val = st.val ∧ (dt.matSt vi st v n).old = st.old

The threaded states differ from the entry state in SAV and TARGET alone – so every hypothesis the atoms need at them is the entry state's.

theorem DescriptiveComplexity.Draw.Data.matSt_fields' {L : FirstOrder.Language} {dt : Data L} {A R P : Type} {vi : dt.VarIx} {st : TapeStD dt A R P} {v : Univ A R P dt.KIx dt.dd → Prop} (n : ℕ) : (dt.matSt vi st v n).new = st.new ∧ (dt.matSt vi st v n).ltp = st.ltp

The same two, along the matrix's whole chain of atoms.

noncomputable def DescriptiveComplexity.Draw.Data.mkKindSem {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [LinearOrder A] [L.Structure A] (zero one : A) (vi : dt.VarIx) (st : TapeStD dt A R P) (w : Fin (dt.nOf vi) → dt.X.Map A) (hENC : ∀ (j : Fin (dt.nOf vi)), wmBlk (dt.lvSet st vi j) (Tag.arg (toLex (dt.lvBlk vi j))) = encMap dt.ly zero one (w j)) (κ : MatAtom dt.X dt.d.B (dt.nOf vi)) : dt.KindSem zero one vi st κ

The semantic data of every atom, from one encoded valuation: the expansion atoms' points are the valuation's, everything else needs nothing.

Equations

• dt.mkKindSem zero one vi st w hENC (DescriptiveComplexity.Draw.MatAtom.eq a a_1) = PUnit.unit
• dt.mkKindSem zero one vi st w hENC (DescriptiveComplexity.Draw.MatAtom.ord a a_1) = PUnit.unit
• dt.mkKindSem zero one vi st w hENC (DescriptiveComplexity.Draw.MatAtom.stage i a) = PUnit.unit
• dt.mkKindSem zero one vi st w hENC (DescriptiveComplexity.Draw.MatAtom.exp a ts) = ⟨fun (ℓ : Fin k) => w (ts ℓ), ⋯⟩

noncomputable def DescriptiveComplexity.Draw.Data.matFsT {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) (vi : dt.VarIx) (st : TapeStD dt A R P) (v : Univ A R P dt.KIx dt.dd → Prop) (enterSt : Fin (dt.natOf vi) → (dt.CtlIx → A) → (dt.SlotIx → A) → dt.CtlIx → A) (sem : (a : Fin (dt.natOf vi)) → dt.KindSem zero one vi (dt.matSt vi st v ↑a) (dt.kindOf vi a)) (f₀ : dt.CtlIx → A) : ℕ → dt.CtlIx → A

The control thread across the matrix's atoms, threaded: as DescriptiveComplexity.Draw.Data.matFs, with each atom's exit control computed at the state that atom actually runs at.

Equations

• One or more equations did not get rendered due to their size.
• dt.matFsT RF hord zero one vi st v enterSt sem f₀ 0 = f₀

theorem DescriptiveComplexity.Draw.Data.scratchEq_matSt {L : FirstOrder.Language} {dt : Data L} {A R P : Type} {vi : dt.VarIx} {st : TapeStD dt A R P} {v : Univ A R P dt.KIx dt.dd → Prop} (n : ℕ) : dt.ScratchEq (dt.matSt vi st v n) st

A threaded state of the matrix is the entry state up to the two scratch registers – matSt_eq in the form the congruences take.

theorem DescriptiveComplexity.Draw.Data.matFs_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} {vi : dt.VarIx} {st : TapeStD dt A R P} {v : Univ A R P dt.KIx dt.dd → Prop} {st' : TapeStD dt A R P} (h : dt.ScratchEq st st') (hreg : ¬∃ (u : Univ A R P dt.KIx dt.dd), v = RF.cell u) (enterSt : Fin (dt.natOf vi) → (dt.CtlIx → A) → (dt.SlotIx → A) → dt.CtlIx → A) (sem : (a : Fin (dt.natOf vi)) → dt.KindSem zero one vi st (dt.kindOf vi a)) (f₀ : dt.CtlIx → A) (n : ℕ) : dt.matFs RF hord zero one vi st v enterSt sem f₀ n = dt.matFs RF hord zero one vi st' v enterSt (fun (a : Fin (dt.natOf vi)) => dt.kindSemCast zero one vi ⋯ ⋯ (dt.kindOf vi a) (sem a)) f₀ n

The matrix is blind to the two scratch registers: atom by atom, kindExitCtl_congr_scratch.

theorem DescriptiveComplexity.Draw.Data.matFsT_eq_matFs {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} {vi : dt.VarIx} {st : TapeStD dt A R P} {v : Univ A R P dt.KIx dt.dd → Prop} (hreg : ¬∃ (u : Univ A R P dt.KIx dt.dd), v = RF.cell u) (enterSt : Fin (dt.natOf vi) → (dt.CtlIx → A) → (dt.SlotIx → A) → dt.CtlIx → A) (semT : (a : Fin (dt.natOf vi)) → dt.KindSem zero one vi (dt.matSt vi st v ↑a) (dt.kindOf vi a)) (f₀ : dt.CtlIx → A) (n : ℕ) : dt.matFsT RF hord zero one vi st v enterSt semT f₀ n = dt.matFs RF hord zero one vi st v enterSt (fun (a : Fin (dt.natOf vi)) => dt.kindSemCast zero one vi ⋯ ⋯ (dt.kindOf vi a) (semT a)) f₀ n

The threaded matrix is the unthreaded one: an atom's machinery reads the levels' registers and its background at the working cell (kindExitCtl_congr_scratch), and the threading rewrites SAV and TARGET alone. This is the bridge between the control the run produces and the control the semantics is stated at.

theorem DescriptiveComplexity.Draw.Data.matrix_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} {st : TapeStD dt A R P} {v : Univ A R P dt.KIx dt.dd → Prop} [Finite dt.KIx] (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') (hwkSt : st.wk = fun (r : Univ A R P dt.KIx dt.dd → Prop) => r = v) (hmirSt : st.mir = v) (hbotSt : st.bot = fun (r : Univ A R P dt.KIx dt.dd → Prop) => r = fun (x : Univ A R P dt.KIx dt.dd) => False) (hsav : st.sav = v) (htgt : st.tgt = v) {emb : dt.MatrixPh vi → P} {exitPh : P} {rEmb : (i : dt.MatrixSite vi) → dt.MatrixSh vi i → R} (enterSt : Fin (dt.natOf vi) → (dt.CtlIx → A) → (dt.SlotIx → A) → dt.CtlIx → A) (hrules : ∀ (i : dt.MatrixSite vi) (ρ : dt.MatrixSh vi i), PR.rules (rEmb i ρ) = dt.matrixRule PR.zero PR.one vi emb (fun (a : Fin (dt.natOf vi)) => dt.atomArgs PR.zero PR.one vi a) enterSt exitPh i ρ) (sem : (a : Fin (dt.natOf vi)) → dt.KindSem PR.zero PR.one vi st (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 (SeqPh.chk 0)) 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.matFs RF hord PR.zero PR.one vi st v enterSt sem f₀ (dt.natOf vi))), 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) }

The matrix's run: from the checkpoint before the first atom at the marker to the exit phase one cell to its right after the last, the verdict slots holding each atom's fold, the tape untouched.

The gates, assembled

noncomputable def DescriptiveComplexity.Draw.Data.gatesFs {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) (st : TapeStD dt A R P) (v : Univ A R P dt.KIx dt.dd → Prop) (bOf : Fin (dt.arOf vi) → Fin dt.ko ⊕ Fin dt.ki) (hc : Fintype.card dt.X.Tag ≤ dt.ntgDim) (hnG : ∀ (t' : dt.X.Tag), (dt.domPk t').n ≤ dt.eDim) (hrdG : ∀ (t' : dt.X.Tag), dt.domNr t' ≤ dt.nfDim) (tOf : Fin (dt.arOf vi) → dt.X.Tag) (enterSt : Fin (dt.arOf vi) → (dt.CtlIx → A) → (dt.SlotIx → A) → dt.CtlIx → A) (f₀ : dt.CtlIx → A) : ℕ → dt.CtlIx → A

The control thread across the gates' blocks (the all-pass path): each block's machinery entered through the dispatch's enterSt, its conjoining exit the next block's input.

Equations

• One or more equations did not get rendered due to their size.
• dt.gatesFs RF zero one vi st v bOf hc hnG hrdG tOf enterSt f₀ 0 = f₀

theorem DescriptiveComplexity.Draw.Data.gates_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} {st : TapeStD dt A R P} {v : Univ A R P dt.KIx dt.dd → Prop} [Finite dt.KIx] (bOf : Fin (dt.arOf vi) → Fin dt.ko ⊕ Fin dt.ki) (hc : Fintype.card dt.X.Tag ≤ dt.ntgDim) (hnG : ∀ (t' : dt.X.Tag), (dt.domPk t').n ≤ dt.eDim) (hrdG : ∀ (t' : dt.X.Tag), dt.domNr t' ≤ dt.nfDim) (wellGOf : Fin (dt.arOf vi) → (dt.SlotIx → A) → Prop) (setFail : (dt.CtlIx → A) → (dt.SlotIx → A) → dt.CtlIx → A) {emb : dt.GatesPh vi → P} {failPh exitPh : P} {rEmb : (i : dt.GatesSite vi) → dt.GatesSh vi i → R} (enterSt : Fin (dt.arOf vi) → (dt.CtlIx → A) → (dt.SlotIx → A) → dt.CtlIx → A) (hrules : ∀ (i : dt.GatesSite vi) (ρ : dt.GatesSh vi i), PR.rules (rEmb i ρ) = dt.gatesRule PR.one vi emb (fun (ℓ : Fin (dt.arOf vi)) => dt.gateArgs PR.zero PR.one (bOf ℓ) hc hnG hrdG) wellGOf setFail enterSt 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' : Univ A R P dt.KIx dt.dd → Prop} (hv : WMSetLt WMLe v (RF.cell gbot)) (hvi : WMIncr WMLe v v') (hwkSt : st.wk = fun (r : Univ A R P dt.KIx dt.dd → Prop) => r = v) (TestOf : Fin (dt.arOf vi) → Univ A R P dt.KIx dt.dd → Prop) (hcompatOf : ∀ (ℓ : Fin (dt.arOf vi)) (u : Univ A R P dt.KIx dt.dd), wellGOf ℓ (PR.passTracksAt RF.cell Slot.mir (dt.back RF.cell PR.zero PR.one ⋯ st) st.mir (RF.cell u)) ↔ TestOf ℓ u) (tOf : Fin (dt.arOf vi) → dt.X.Tag) (htagOf : ∀ (ℓ : Fin (dt.arOf vi)), dt.dspTagOf PR.zero PR.one (wmBlk st.mir (Tag.arg (toLex (bOf ℓ)))) = tOf ℓ) (hTestOf : ∀ (ℓ : Fin (dt.arOf vi)) (u : Univ A R P dt.KIx dt.dd), TestOf ℓ u) (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 ⋯ st) st.val) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt exitPh (dt.gatesFs RF PR.zero PR.one vi st v bOf hc hnG hrdG tOf enterSt f₀ (dt.arOf vi))), 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) }

The gates' run at a gated address: every block passes its shape test, every domain evaluation runs on its block's decoded tag, and the sequence exits with the conjoined verdict in the flag.