The two scratch registers are parked at the marker

DescriptiveComplexity.Draw.Data.ixLegStB_fields says a leg of the spine leaves the mirror, the working register, the bottom mark, the stage tracks and the last-pass flag alone. It says nothing about the two scratch registers, SAV and TARGET, because a leg does write them – and the evaluation's exit asks that they be back at the marker when the spine is over (hsavL, htgtL).

This file closes that: an atom parks both at the marker when it is a stage atom and touches neither otherwise (ixKindEndSt), so a state entered with them parked leaves with them parked, and the property rides the matrix's chain, the round, the VAL loop's thread and the whole branched spine. The marker being the empty address, the entry state has them parked for free.

def DescriptiveComplexity.Draw.Data.Parked {L : FirstOrder.Language} (dt : Data L) {A R P I : Type} (st : TapeSt dt A R P I) (elt : I → Univ A R P dt.KIx dt.dd) (v : Univ A R P dt.KIx dt.dd → Prop) : Prop

Both scratch registers are parked at the marker.

Equations

• dt.Parked st elt v = (st.sav = DescriptiveComplexity.ixMark elt v ∧ st.tgt = DescriptiveComplexity.ixMark elt v)

theorem DescriptiveComplexity.Draw.Data.parked_ixKindEndSt {L : FirstOrder.Language} {dt : Data L} {A R P I : Type} {elt : I → Univ A R P dt.KIx dt.dd} {v : Univ A R P dt.KIx dt.dd → Prop} {vi : dt.VarIx} {st : TapeSt dt A R P I} (κ : MatAtom dt.X dt.d.B (dt.nOf vi)) (hst : dt.Parked st elt v) : dt.Parked (dt.ixKindEndSt vi v κ st) elt v

An atom leaves the scratch parked: a stage atom parks both registers at the marker, and every other kind touches neither.

theorem DescriptiveComplexity.Draw.Data.parked_ixMatSt {L : FirstOrder.Language} {dt : Data L} {A R P I : Type} {elt : I → Univ A R P dt.KIx dt.dd} {v : Univ A R P dt.KIx dt.dd → Prop} {vi : dt.VarIx} {st : TapeSt dt A R P I} (hst : dt.Parked st elt v) (n : ℕ) : dt.Parked (dt.ixMatSt vi st v n) elt v

The matrix's chain leaves the scratch parked.

theorem DescriptiveComplexity.Draw.Data.parked_ixRoundEndSt {L : FirstOrder.Language} {dt : Data L} {A R P I : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] [Nonempty A] [L.IsRelational] [L.Structure A] {elt : I → Univ A R P dt.KIx dt.dd} {v : Univ A R P dt.KIx dt.dd → Prop} {F : LaidFile dt A R P I} {zero one : A} {hhas : F.toLayout.HasName zero} {vi : dt.VarIx} {stV : TapeSt dt A R P I} (hst : dt.Parked stV elt v) (f₀ : dt.CtlIx → A) : dt.Parked (dt.ixRoundEndSt F zero one hhas vi stV v f₀) elt v

A round leaves the scratch parked: it is the matrix's chain when the gates pass and the identity when they do not.

Up the tower: the VAL loop, the leg and the spine

theorem DescriptiveComplexity.Draw.Data.parked_ixVarSTT {L : FirstOrder.Language} {dt : Data L} {A R P I : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] [Nonempty A] [L.IsRelational] [L.Structure A] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} {elt : I → Univ A R P dt.KIx dt.dd} {v : Univ A R P dt.KIx dt.dd → Prop} (F : LaidFile dt A R P I) (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)) {ιV : Type} [LinearOrder ιV] (mV : ιV → I → Prop) {vi : dt.VarIx} {st : TapeSt dt A R P I} {semT : (p : dt.IxScratch A R P I) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn vi)), dt.ixIGPassP F PR.zero PR.one vi (ixVarRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf vi)) → dt.IxKindSem PR.zero PR.one vi (dt.ixMatSt vi (ixVarRdSt st p (mV a)) v ↑b) elt (dt.kindOf vi b)} (hst : dt.Parked st elt v) (fG : dt.CtlIx → A) (a : ιV) : (ixVarSTT F hinj hhasP heltP vi st v mV semT fG a).1 = ixMark elt v ∧ (ixVarSTT F hinj hhasP heltP vi st v mV semT fG a).2 = ixMark elt v

The VAL loop's thread leaves the scratch parked: the pair it carries is the round's, and a round parks both registers.

theorem DescriptiveComplexity.Draw.Data.parked_ixVarStE {L : FirstOrder.Language} {dt : Data L} {A R P I : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] [Nonempty A] [L.IsRelational] [L.Structure A] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} {elt : I → Univ A R P dt.KIx dt.dd} {v : Univ A R P dt.KIx dt.dd → Prop} (F : LaidFile dt A R P I) (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)) {ιV : Type} [LinearOrder ιV] (mV : ιV → I → Prop) {vi : dt.VarIx} {st : TapeSt dt A R P I} {semT : (p : dt.IxScratch A R P I) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn vi)), dt.ixIGPassP F PR.zero PR.one vi (ixVarRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf vi)) → dt.IxKindSem PR.zero PR.one vi (dt.ixMatSt vi (ixVarRdSt st p (mV a)) v ↑b) elt (dt.kindOf vi b)} (hst : dt.Parked st elt v) (fG : dt.CtlIx → A) (a : ιV) : dt.Parked (ixVarStE F hinj hhasP heltP vi st v mV semT fG a) elt v

A VAL round's exit state leaves the scratch parked.

theorem DescriptiveComplexity.Draw.Data.parked_ixLegStB {L : FirstOrder.Language} {dt : Data L} {A R P I : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] [Nonempty A] [L.IsRelational] [L.Structure A] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} {elt : I → Univ A R P dt.KIx dt.dd} {v : Univ A R P dt.KIx dt.dd → Prop} (F : LaidFile dt A R P I) (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)) {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → I → Prop) {j : Fin dt.nv} {st : TapeSt dt A R P I} {semT : dt.ixGatedAt F j st → (p : dt.IxScratch A R P I) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.ixIGPassP F PR.zero PR.one (dt.varAt j) (ixVarRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.IxKindSem PR.zero PR.one (dt.varAt j) (dt.ixMatSt (dt.varAt j) (ixVarRdSt st p (mV a)) v ↑b) elt (dt.kindOf (dt.varAt j) b)} (hst : dt.Parked st elt v) (f₀ : dt.CtlIx → A) : dt.Parked (dt.ixLegStB F hinj hhasP heltP mV j st semT f₀) elt v

A leg leaves the scratch parked: gated, it is the VAL loop's exit state with the stage bit written; ungated, it writes nothing but that bit.

theorem DescriptiveComplexity.Draw.Data.parked_ixSpineStOfB {L : FirstOrder.Language} {dt : Data L} {A R P I : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] [Nonempty A] [L.IsRelational] [L.Structure A] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} {elt : I → Univ A R P dt.KIx dt.dd} {v : Univ A R P dt.KIx dt.dd → Prop} (F : LaidFile dt A R P I) (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)) {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → I → Prop) {st₀ : TapeSt dt A R P I} {f₀ : dt.CtlIx → A} {semB : (w : Univ A R P dt.KIx dt.dd → Prop) → (j : Fin dt.nv) → (st : TapeSt dt A R P I) → dt.ixGatedAt F j st → (p : dt.IxScratch A R P I) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.ixIGPassP F PR.zero PR.one (dt.varAt j) (ixVarRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.IxKindSem PR.zero PR.one (dt.varAt j) (dt.ixMatSt (dt.varAt j) (ixVarRdSt st p (mV a)) w ↑b) elt (dt.kindOf (dt.varAt j) b)} (hst₀ : dt.Parked st₀ elt v) (k : Fin (dt.nv + 1)) : dt.Parked (dt.ixSpineStOfB F hinj hhasP heltP mV st₀ f₀ semB k) elt v

The branched spine leaves the scratch parked, position by position: the hsavL and htgtL an evaluation's exit asks for, at any file.