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_reachesIn {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) (w : ℕ) (hStage : ∀ (a : Fin n), (wideData (Univ A R P K dd)).ReachesIn w { 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) }) : (wideData (Univ A R P K dd)).ReachesIn ((w + 2) * n + 1) { 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, on a clock: from the checkpoint before the first stage at the marker to the exit phase one cell to its right after the last stage, at each stage's own width plus the dispatch and the walk back, and one step to leave.

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.

theorem DescriptiveComplexity.Draw.seq_run_prefix {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) (j : Fin (n + 1)) (hStageLt : ∀ (a : Fin n), ↑a < ↑j → 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 (emb (SeqPh.chk j)) (fs j)), head := Sum.inl v, tape := wideTape (PR.trackTapeAt RF.cell t₀ (restOf j) (mOf j)) (PR.syElt PR.blank) }

The sequencer's prefix: from the checkpoint before the first stage to any later checkpoint, given the stages strictly below it – what a run that leaves the sequence early (a failing gate block) composes with.

theorem DescriptiveComplexity.Draw.seq_reachesIn_prefix {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) (w : ℕ) (j : Fin (n + 1)) (hStageLt : ∀ (a : Fin n), ↑a < ↑j → (wideData (Univ A R P K dd)).ReachesIn w { 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) }) : (wideData (Univ A R P K dd)).ReachesIn ((w + 2) * ↑j) { 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 (emb (SeqPh.chk j)) (fs j)), head := Sum.inl v, tape := wideTape (PR.trackTapeAt RF.cell t₀ (restOf j) (mOf j)) (PR.syElt PR.blank) }

The sequencer's prefix, on a clock: as DescriptiveComplexity.Draw.seq_run_prefix with the stages counted – a stage's own width, its dispatch and the step back, once per stage below the checkpoint.