The sequencer's run

The run theorem of DescriptiveComplexity.Draw.seqRule: from the checkpoint before the first stage at the marker, one abstract stage run per position, to the exit phase one cell to the marker's right after the last – the matrix runs its classified atoms with it, the gates their blocks, and neither needs to know a stage's internals beyond its entry phase and its control and tape transforms.

The run comes with its cost (seq_reachesIn): a stage's own width plus the dispatch and the walk back, once per stage, and one step to leave. seq_run is it with the budget forgotten – the widths recovered from the stages' runs by DescriptiveComplexity.TMData.exists_reachesIn_of_reflTransGen and the largest taken, which is why a space-bounded caller need not have counted anything.

theorem DescriptiveComplexity.Draw.seq_run {A R P Q W K : Type} {dd n : ℕ} {PA SA : Fin n → Type} {ShA : (a : Fin n) → SA a → Type} [Fintype Q] [Fintype W] [DecidableEq W] [LinearOrder A] [LinearOrder R] [LinearOrder P] [LinearOrder K] [FirstOrder.Language.wide.Structure (Univ A R P K dd)] [Finite A] [Finite R] [Finite P] [Finite K] {PR : Prog A R P Q W K dd} {I : Type} {ile : I → I → Prop} (RF : IxFile (Univ A R P K dd) I ile) {wk rg : W} {emb : SeqPh n PA → P} {ruleA : (a : Fin n) → (s : SA a) → ShA a s → Rule A Q W P} {entry : (a : Fin n) → PA a} {enterSt : Fin n → (Q → A) → (W → A) → Q → A} {exitPh : P} {rEmb : (i : SeqSite n SA) → SeqSh n ShA i → R} (hrules : ∀ (i : SeqSite n SA) (ρ : SeqSh n ShA i), PR.rules (rEmb i ρ) = seqRule PR.one wk rg emb ruleA entry enterSt exitPh i ρ) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) (hix : IsLinOrd ile) {gbot : I} (hbot : ∀ (y : I), ile gbot y) {v v' : Univ A R P K dd → Prop} (hv : WMSetLt WMLe v (RF.cell gbot)) (hvi : WMIncr WMLe v v') {t₀ : W} {restOf : Fin (n + 1) → (Univ A R P K dd → Prop) → W → A} {mOf : Fin (n + 1) → I → Prop} (hwkOf : ∀ (k : Fin (n + 1)) (r : Univ A R P K dd → Prop), restOf k r wk = bitVal PR.zero PR.one (r = v)) (hrgOf : ∀ (k : Fin (n + 1)) (r : Univ A R P K dd → Prop), restOf k r rg = bitVal PR.zero PR.one (∃ (u : I), r = RF.cell u)) (hmOf : ∀ (k : Fin (n + 1)) (r : Univ A R P K dd → Prop), restOf k r t₀ = bitVal PR.zero PR.one (bitAtOf RF.cell (mOf k) r)) (hwkt₀ : wk ≠ t₀) (hrgt₀ : rg ≠ t₀) (fs : Fin (n + 1) → Q → A) (hStageR : ∀ (a : Fin n), Relation.ReflTransGen (wideData (Univ A R P K dd)).Step { state := Sum.inr (PR.stElt (emb (SeqPh.sub a (entry a))) (enterSt a (fs a.castSucc) (restOf a.castSucc v))), head := Sum.inl v', tape := wideTape (PR.trackTapeAt RF.cell t₀ (restOf a.castSucc) (mOf a.castSucc)) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (emb (SeqPh.chk a.succ)) (fs a.succ)), head := Sum.inl v', tape := wideTape (PR.trackTapeAt RF.cell t₀ (restOf a.succ) (mOf a.succ)) (PR.syElt PR.blank) }) : Relation.ReflTransGen (wideData (Univ A R P K dd)).Step { state := Sum.inr (PR.stElt (emb (SeqPh.chk 0)) (fs 0)), head := Sum.inl v, tape := wideTape (PR.trackTapeAt RF.cell t₀ (restOf 0) (mOf 0)) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt exitPh (fs (Fin.last n))), head := Sum.inl v', tape := wideTape (PR.trackTapeAt RF.cell t₀ (restOf (Fin.last n)) (mOf (Fin.last n))) (PR.syElt PR.blank) }

The sequencer's run, the budget forgotten: what a space-bounded caller reads, its stages' runs carrying no count.