Resetting the working cell to the bottom

A random access starts at the checkpoint: marker and mirror at the empty address. Getting there from wherever the marker is – DescriptiveComplexity.Draw.Prog.reaches_reset – is the one itinerary of the program that runs down the working area: erase the marker and step right (never left, so the empty address needs no special case), scan left to the cell the permanent bot mark identifies, write the marker there stepping right, and bounce back left onto it. The mirror is cleared by a separate DescriptiveComplexity.Draw.ClearKit trip afterwards.

DescriptiveComplexity.Draw.ResetKit is the kit: the scan and the two bounce steps; the erasing entry is the caller's rule, and the landing phase hosts nothing – the machine arrives exactly once, at the bottom cell, where the caller's exit fires.

theorem DescriptiveComplexity.Draw.Prog.reachesIn_reset {A R P Q W K : Type} {dd : ℕ} [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) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) {t bt wk : W} (hnebt : bt ≠ t) (hnewk : wk ≠ t) {v : Univ A R P K dd → Prop} (hv : ∃ (x : Univ A R P K dd), ¬v x) {m : I → Prop} {restA restN restB : (Univ A R P K dd → Prop) → W → A} (hAN : ∀ (r : Univ A R P K dd → Prop), r ≠ v → restN r = restA r) (hNB : ∀ (r : Univ A R P K dd → Prop), (r ≠ fun (x : Univ A R P K dd) => False) → restB r = restN r) (hbtN : ∀ (r : Univ A R P K dd → Prop), restN r bt = bitVal PR.zero PR.one (r = fun (x : Univ A R P K dd) => False)) (hwkB : ∀ (r : Univ A R P K dd → Prop), restB r wk = bitVal PR.zero PR.one (r = fun (x : Univ A R P K dd) => False)) (hNBslot : ∀ (s : W), s ≠ wk → restB (fun (x : Univ A R P K dd) => False) s = restN (fun (x : Univ A R P K dd) => False) s) {p₀ pScan pB pDone : P} {fc : Q → A} (h₀ : PR.HasRight p₀ fc (PR.passTracksAt RF.cell t restA m v) pScan fc (PR.passTracksAt RF.cell t restN m v)) (hdown : ∀ (g : W → A), g bt ≠ PR.one → PR.HasLeft pScan fc g pScan fc g) (hput : ∀ (g : W → A), g bt = PR.one → PR.HasRight pScan fc g pB fc (Function.update g wk PR.one)) (hback : ∀ (g : W → A), PR.HasLeft pB fc g pDone fc g) : (wideData (Univ A R P K dd)).ReachesIn (wideRank v + 4) { state := Sum.inr (PR.stElt p₀ fc), head := Sum.inl v, tape := wideTape (PR.trackTapeAt RF.cell t restA m) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt pDone fc), head := Sum.inl fun (x : Univ A R P K dd) => False, tape := wideTape (PR.trackTapeAt RF.cell t restB m) (PR.syElt PR.blank) }

The reset, on a clock: from the caller's phase at the marker – whose erasing step, rightwards, is the caller's rule – scan left to the bottom cell, write the marker there stepping right, and bounce back onto it. The empty address is identified by the permanent bot mark, and no leftward step is ever taken at it. The scan is a walk down the whole order below the marker, so the cost is the marker's rank and the three steps around it.

theorem DescriptiveComplexity.Draw.Prog.reaches_reset {A R P Q W K : Type} {dd : ℕ} [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) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) {t bt wk : W} (hnebt : bt ≠ t) (hnewk : wk ≠ t) {v : Univ A R P K dd → Prop} (hv : ∃ (x : Univ A R P K dd), ¬v x) {m : I → Prop} {restA restN restB : (Univ A R P K dd → Prop) → W → A} (hAN : ∀ (r : Univ A R P K dd → Prop), r ≠ v → restN r = restA r) (hNB : ∀ (r : Univ A R P K dd → Prop), (r ≠ fun (x : Univ A R P K dd) => False) → restB r = restN r) (hbtN : ∀ (r : Univ A R P K dd → Prop), restN r bt = bitVal PR.zero PR.one (r = fun (x : Univ A R P K dd) => False)) (hwkB : ∀ (r : Univ A R P K dd → Prop), restB r wk = bitVal PR.zero PR.one (r = fun (x : Univ A R P K dd) => False)) (hNBslot : ∀ (s : W), s ≠ wk → restB (fun (x : Univ A R P K dd) => False) s = restN (fun (x : Univ A R P K dd) => False) s) {p₀ pScan pB pDone : P} {fc : Q → A} (h₀ : PR.HasRight p₀ fc (PR.passTracksAt RF.cell t restA m v) pScan fc (PR.passTracksAt RF.cell t restN m v)) (hdown : ∀ (g : W → A), g bt ≠ PR.one → PR.HasLeft pScan fc g pScan fc g) (hput : ∀ (g : W → A), g bt = PR.one → PR.HasRight pScan fc g pB fc (Function.update g wk PR.one)) (hback : ∀ (g : W → A), PR.HasLeft pB fc g pDone fc g) : Relation.ReflTransGen (wideData (Univ A R P K dd)).Step { state := Sum.inr (PR.stElt p₀ fc), head := Sum.inl v, tape := wideTape (PR.trackTapeAt RF.cell t restA m) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt pDone fc), head := Sum.inl fun (x : Univ A R P K dd) => False, tape := wideTape (PR.trackTapeAt RF.cell t restB m) (PR.syElt PR.blank) }

The reset, the budget forgotten.

The reset kit

inductive DescriptiveComplexity.Draw.ResetPh : Type

The phases of a reset: the down-scan, the bounce, and the landing – which hosts no rule, the caller's exit firing on arrival.

• scan : ResetPh

  Scanning left to the bottom cell.

• b : ResetPh

  The marker written, bouncing back.

• done : ResetPh

  At the bottom cell, marker set.

@[instance_reducible]

instance DescriptiveComplexity.Draw.instDecidableEqResetPh : DecidableEq ResetPh

Equations

• DescriptiveComplexity.Draw.instDecidableEqResetPh x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance DescriptiveComplexity.Draw.instFiniteResetPh : Finite ResetPh

inductive DescriptiveComplexity.Draw.ResetRule : Type

The rule families of a reset.

• down : ResetRule

  Scan left while the bottom mark is clear.

• put : ResetRule

  At the bottom cell: write the marker, step right.

• back : ResetRule

  Bounce back left onto the marker.

@[instance_reducible]

instance DescriptiveComplexity.Draw.instDecidableEqResetRule : DecidableEq ResetRule

Equations

• DescriptiveComplexity.Draw.instDecidableEqResetRule x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance DescriptiveComplexity.Draw.instFiniteResetRule : Finite ResetRule

structure DescriptiveComplexity.Draw.ResetKit (A Q W P : Type) : Type

A reset kit: the walked track, the bottom-mark and marker slots, and the phases.

• t : W

  The walked track (rides along unchanged).

• bt : W

  The bottom mark, planted at the empty address at startup.

• wk : W

  The working-cell marker slot.

• emb : ResetPh → P

  The kit's phases in the program.

noncomputable def DescriptiveComplexity.Draw.ResetKit.rule {A Q W P : Type} [DecidableEq W] (κ : ResetKit A Q W P) (one : A) : ResetRule → Rule A Q W P

The kit's rules.

Equations

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

theorem DescriptiveComplexity.Draw.ResetKit.dstPh_emb {A Q W P : Type} [DecidableEq W] (κ : ResetKit A Q W P) (one : A) (ρ : ResetRule) : ∃ (p : ResetPh), (κ.rule one ρ).dstPh = κ.emb p

A reset stays inside its own phases: every rule of the kit lands in one of the three the kit was given.

theorem DescriptiveComplexity.Draw.ResetKit.sep {A Q W P : Type} [DecidableEq W] (κ : ResetKit A Q W P) (one : A) (hemb : Function.Injective κ.emb) (ρ ρ' : ResetRule) (f : Q → A) (g : W → A) : (κ.rule one ρ).guard f g → (κ.rule one ρ').guard f g → (κ.rule one ρ).srcPh = (κ.rule one ρ').srcPh → ρ = ρ'

In-shape separation.

theorem DescriptiveComplexity.Draw.ResetKit.exit_disjoint {A Q W P : Type} [DecidableEq W] (κ : ResetKit A Q W P) (one : A) (hemb : Function.Injective κ.emb) (ρ : ResetRule) (f : Q → A) (g : W → A) : (κ.rule one ρ).guard f g → (κ.rule one ρ).srcPh = κ.emb ResetPh.done → False

Exit disjointness at the landing phase: no kit rule fires from it at all.

theorem DescriptiveComplexity.Draw.ResetKit.reachesIn {A R P Q W K : Type} {dd : ℕ} [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} {κ : ResetKit A Q W P} {I : Type} {ile : I → I → Prop} (RF : IxFile (Univ A R P K dd) I ile) {rEmb : ResetRule → R} (hrules : ∀ (ρ : ResetRule), PR.rules (rEmb ρ) = κ.rule PR.one ρ) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) (hnebt : κ.bt ≠ κ.t) (hnewk : κ.wk ≠ κ.t) {v : Univ A R P K dd → Prop} (hv : ∃ (x : Univ A R P K dd), ¬v x) {m : I → Prop} {restA restN restB : (Univ A R P K dd → Prop) → W → A} (hAN : ∀ (r : Univ A R P K dd → Prop), r ≠ v → restN r = restA r) (hNB : ∀ (r : Univ A R P K dd → Prop), (r ≠ fun (x : Univ A R P K dd) => False) → restB r = restN r) (hbtN : ∀ (r : Univ A R P K dd → Prop), restN r κ.bt = bitVal PR.zero PR.one (r = fun (x : Univ A R P K dd) => False)) (hwkB : ∀ (r : Univ A R P K dd → Prop), restB r κ.wk = bitVal PR.zero PR.one (r = fun (x : Univ A R P K dd) => False)) (hNBslot : ∀ (s : W), s ≠ κ.wk → restB (fun (x : Univ A R P K dd) => False) s = restN (fun (x : Univ A R P K dd) => False) s) {p₀ : P} {fc : Q → A} (h₀ : PR.HasRight p₀ fc (PR.passTracksAt RF.cell κ.t restA m v) (κ.emb ResetPh.scan) fc (PR.passTracksAt RF.cell κ.t restN m v)) : (wideData (Univ A R P K dd)).ReachesIn (wideRank v + 4) { state := Sum.inr (PR.stElt p₀ fc), head := Sum.inl v, tape := wideTape (PR.trackTapeAt RF.cell κ.t restA m) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (κ.emb ResetPh.done) fc), head := Sum.inl fun (x : Univ A R P K dd) => False, tape := wideTape (PR.trackTapeAt RF.cell κ.t restB m) (PR.syElt PR.blank) }

The kit resets the marker to the bottom, on a clock: from the caller's phase at the marker – whose erasing step is the caller's rule, the one hypothesis beyond the slot equations – to the landing phase on the empty address, down the whole order below the marker.

theorem DescriptiveComplexity.Draw.ResetKit.reaches {A R P Q W K : Type} {dd : ℕ} [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} {κ : ResetKit A Q W P} {I : Type} {ile : I → I → Prop} (RF : IxFile (Univ A R P K dd) I ile) {rEmb : ResetRule → R} (hrules : ∀ (ρ : ResetRule), PR.rules (rEmb ρ) = κ.rule PR.one ρ) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) (hnebt : κ.bt ≠ κ.t) (hnewk : κ.wk ≠ κ.t) {v : Univ A R P K dd → Prop} (hv : ∃ (x : Univ A R P K dd), ¬v x) {m : I → Prop} {restA restN restB : (Univ A R P K dd → Prop) → W → A} (hAN : ∀ (r : Univ A R P K dd → Prop), r ≠ v → restN r = restA r) (hNB : ∀ (r : Univ A R P K dd → Prop), (r ≠ fun (x : Univ A R P K dd) => False) → restB r = restN r) (hbtN : ∀ (r : Univ A R P K dd → Prop), restN r κ.bt = bitVal PR.zero PR.one (r = fun (x : Univ A R P K dd) => False)) (hwkB : ∀ (r : Univ A R P K dd → Prop), restB r κ.wk = bitVal PR.zero PR.one (r = fun (x : Univ A R P K dd) => False)) (hNBslot : ∀ (s : W), s ≠ κ.wk → restB (fun (x : Univ A R P K dd) => False) s = restN (fun (x : Univ A R P K dd) => False) s) {p₀ : P} {fc : Q → A} (h₀ : PR.HasRight p₀ fc (PR.passTracksAt RF.cell κ.t restA m v) (κ.emb ResetPh.scan) fc (PR.passTracksAt RF.cell κ.t restN m v)) : Relation.ReflTransGen (wideData (Univ A R P K dd)).Step { state := Sum.inr (PR.stElt p₀ fc), head := Sum.inl v, tape := wideTape (PR.trackTapeAt RF.cell κ.t restA m) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (κ.emb ResetPh.done) fc), head := Sum.inl fun (x : Univ A R P K dd) => False, tape := wideTape (PR.trackTapeAt RF.cell κ.t restB m) (PR.syElt PR.blank) }

The kit resets the marker to the bottom, the budget forgotten.

Going home

After a plain sweep the machine stands at the top of the stretch while the marker never moved: getting back is a scan, not a reset. One phase, one rule – walk left unless the marker is under the head – and the caller's exit fires on arrival.

theorem DescriptiveComplexity.Draw.Prog.reachesIn_home {A R P Q W K : Type} {dd : ℕ} [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) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) {t wk : W} (hnewk : wk ≠ t) {rest : (Univ A R P K dd → Prop) → W → A} {m : I → Prop} {v : Univ A R P K dd → Prop} (hwkS : ∀ (r : Univ A R P K dd → Prop), rest r wk = bitVal PR.zero PR.one (r = v)) {p : P} {fc : Q → A} (hdown : ∀ (r : Univ A R P K dd → Prop), PR.passTracksAt RF.cell t rest m r wk ≠ PR.one → PR.HasLeft p fc (PR.passTracksAt RF.cell t rest m r) p fc (PR.passTracksAt RF.cell t rest m r)) {s : Univ A R P K dd → Prop} (hle : WMSetLe WMLe v s) : (wideData (Univ A R P K dd)).ReachesIn (wideRank s - wideRank v) { state := Sum.inr (PR.stElt p fc), head := Sum.inl s, tape := wideTape (PR.trackTapeAt RF.cell t rest m) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt p fc), head := Sum.inl v, tape := wideTape (PR.trackTapeAt RF.cell t rest m) (PR.syElt PR.blank) }

The walk home, on a budget: from anywhere at or above the marker, scan left to it, in the difference of the two ranks. The marker's cell is identified by its own slot, and nothing on the way is rewritten.

theorem DescriptiveComplexity.Draw.Prog.reaches_home {A R P Q W K : Type} {dd : ℕ} [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) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) {t wk : W} (hnewk : wk ≠ t) {rest : (Univ A R P K dd → Prop) → W → A} {m : I → Prop} {v : Univ A R P K dd → Prop} (hwkS : ∀ (r : Univ A R P K dd → Prop), rest r wk = bitVal PR.zero PR.one (r = v)) {p : P} {fc : Q → A} (hdown : ∀ (r : Univ A R P K dd → Prop), PR.passTracksAt RF.cell t rest m r wk ≠ PR.one → PR.HasLeft p fc (PR.passTracksAt RF.cell t rest m r) p fc (PR.passTracksAt RF.cell t rest m r)) {s : Univ A R P K dd → Prop} (hle : WMSetLe WMLe v s) : Relation.ReflTransGen (wideData (Univ A R P K dd)).Step { state := Sum.inr (PR.stElt p fc), head := Sum.inl s, tape := wideTape (PR.trackTapeAt RF.cell t rest m) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt p fc), head := Sum.inl v, tape := wideTape (PR.trackTapeAt RF.cell t rest m) (PR.syElt PR.blank) }

The walk home: from anywhere at or above the marker, scan left to it. The marker's cell is identified by its own slot, and nothing on the way is rewritten.

structure DescriptiveComplexity.Draw.HomeKit (A Q W P : Type) : Type

A home kit: one phase, one rule – walk left unless the marker is under the head. The caller's exit, guarded wk = one ∧ rg ≠ one, is disjoint by construction.

• t : W

  The walked track (rides along unchanged).

• wk : W

  The working-cell marker slot.

• ph : P

  The kit's phase in the program.

inductive DescriptiveComplexity.Draw.HomeKit.HomeRule : Type

The rule of a home kit.

• down : HomeRule

  Walk left unless the marker is under the head.

@[instance_reducible]

instance DescriptiveComplexity.Draw.HomeKit.instDecidableEqHomeRule : DecidableEq HomeRule

Equations

• DescriptiveComplexity.Draw.HomeKit.instDecidableEqHomeRule x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance DescriptiveComplexity.Draw.HomeKit.instFiniteHomeRule : Finite HomeRule

def DescriptiveComplexity.Draw.HomeKit.rule {A Q W P : Type} (κ : HomeKit A Q W P) (one : A) : HomeRule → Rule A Q W P

The kit's rule.

Equations

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

theorem DescriptiveComplexity.Draw.HomeKit.sep {A Q W P : Type} (κ : HomeKit A Q W P) (one : A) (ρ ρ' : HomeRule) (f : Q → A) (g : W → A) : (κ.rule one ρ).guard f g → (κ.rule one ρ').guard f g → (κ.rule one ρ).srcPh = (κ.rule one ρ').srcPh → ρ = ρ'

In-shape separation: one rule, nothing to separate.

theorem DescriptiveComplexity.Draw.HomeKit.exit_disjoint {A Q W P : Type} (κ : HomeKit A Q W P) (one : A) (ρ : HomeRule) (f : Q → A) (g : W → A) : (κ.rule one ρ).guard f g → g κ.wk = one → False

Exit disjointness: the rule never fires at the marker.

theorem DescriptiveComplexity.Draw.HomeKit.reachesIn {A R P Q W K : Type} {dd : ℕ} [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} {κ : HomeKit A Q W P} {I : Type} {ile : I → I → Prop} (RF : IxFile (Univ A R P K dd) I ile) {rEmb : HomeRule → R} (hrules : ∀ (ρ : HomeRule), PR.rules (rEmb ρ) = κ.rule PR.one ρ) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) (hnewk : κ.wk ≠ κ.t) {rest : (Univ A R P K dd → Prop) → W → A} {m : I → Prop} {v : Univ A R P K dd → Prop} (hwkS : ∀ (r : Univ A R P K dd → Prop), rest r κ.wk = bitVal PR.zero PR.one (r = v)) {fc : Q → A} {s : Univ A R P K dd → Prop} (hle : WMSetLe WMLe v s) : (wideData (Univ A R P K dd)).ReachesIn (wideRank s - wideRank v) { state := Sum.inr (PR.stElt κ.ph fc), head := Sum.inl s, tape := wideTape (PR.trackTapeAt RF.cell κ.t rest m) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt κ.ph fc), head := Sum.inl v, tape := wideTape (PR.trackTapeAt RF.cell κ.t rest m) (PR.syElt PR.blank) }

The kit walks home, on a budget: from anywhere at or above the marker, down to it, in the difference of the two ranks.

theorem DescriptiveComplexity.Draw.HomeKit.reaches {A R P Q W K : Type} {dd : ℕ} [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} {κ : HomeKit A Q W P} {I : Type} {ile : I → I → Prop} (RF : IxFile (Univ A R P K dd) I ile) {rEmb : HomeRule → R} (hrules : ∀ (ρ : HomeRule), PR.rules (rEmb ρ) = κ.rule PR.one ρ) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) (hnewk : κ.wk ≠ κ.t) {rest : (Univ A R P K dd → Prop) → W → A} {m : I → Prop} {v : Univ A R P K dd → Prop} (hwkS : ∀ (r : Univ A R P K dd → Prop), rest r κ.wk = bitVal PR.zero PR.one (r = v)) {fc : Q → A} {s : Univ A R P K dd → Prop} (hle : WMSetLe WMLe v s) : Relation.ReflTransGen (wideData (Univ A R P K dd)).Step { state := Sum.inr (PR.stElt κ.ph fc), head := Sum.inl s, tape := wideTape (PR.trackTapeAt RF.cell κ.t rest m) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt κ.ph fc), head := Sum.inl v, tape := wideTape (PR.trackTapeAt RF.cell κ.t rest m) (PR.syElt PR.blank) }

The kit walks home: from anywhere at or above the marker, down to it.