The advance kit: one round of a sweep

The kit wrapping DescriptiveComplexity.Draw.Prog.reaches_fileAdvance – the round every sweep of the EXPSPACE program repeats: erase the working-cell marker and step right, write it at the next address and step on, scan up to the file top, bounce, run the mirror increment down the file, scan back to the marker.

The first of those steps is fired from the caller's phase – the phase that decided to advance – so it is a hypothesis of the discharge, not a kit rule (rules are owned by their source phase). Everything after it is the kit's: the marker write is the single rule of a dedicated phase (guard ⊤, the phase is only ever entered on the fresh marker cell), and the increment and return rules are the ones the third hardening shaped, with the landing phase's single rg = one ∨ wk ≠ one rule serving hold, walk and return.

The advance's shapes

inductive DescriptiveComplexity.Draw.AdvPh : Type

The phases of an advance: past the erased marker, scanning up, bounced, carrying, and landed.

• a1 : AdvPh

  On the fresh marker cell, about to write it.

• a2 : AdvPh

  Scanning up to the file top.

• a2b : AdvPh

  Bounced off the top, about to re-enter rightwards.

• a3 : AdvPh

  Running the increment: clearing set digits.

• a4 : AdvPh

  The increment landed: walking home.

@[instance_reducible]

instance DescriptiveComplexity.Draw.instDecidableEqAdvPh : DecidableEq AdvPh

Equations

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

instance DescriptiveComplexity.Draw.instFiniteAdvPh : Finite AdvPh

inductive DescriptiveComplexity.Draw.AdvRule : Type

The rule families of an advance.

• put1 : AdvRule

  Write the marker at the fresh cell, stepping on.

• up : AdvRule

  Scan right while the file-top mark is clear.

• b1 : AdvRule

  At the file top: step left into the bounce phase.

• b2go : AdvRule

  Bounce: step back right into the increment.

• clear : AdvRule

  At a register with a set digit: clear it, carry on.

• set : AdvRule

  At a register with a clear digit: set it, land.

• walk : AdvRule

  Walk left over unmarked cells while carrying.

• stay : AdvRule

  Hold at registers, walk and return, once landed.

@[instance_reducible]

instance DescriptiveComplexity.Draw.instDecidableEqAdvRule : DecidableEq AdvRule

Equations

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

instance DescriptiveComplexity.Draw.instFiniteAdvRule : Finite AdvRule

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

An advance kit: the walked mirror track, the service slots, and the phases.

• t : W

  The walked mirror track.

• rg : W

  The register mark.

• rl : W

  The file-top mark.

• wk : W

  The working-cell marker slot.

• emb : AdvPh → P

  The kit's phases in the program.

def DescriptiveComplexity.Draw.AdvKit.rule {A Q W P : Type} [DecidableEq W] (κ : AdvKit A Q W P) (zero one : A) : AdvRule → 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.AdvKit.sep {A Q W P : Type} [DecidableEq W] (κ : AdvKit A Q W P) (zero one : A) (hzo : zero ≠ one) (hemb : Function.Injective κ.emb) (ρ ρ' : AdvRule) (f : Q → A) (g : W → A) : (κ.rule zero one ρ).guard f g → (κ.rule zero one ρ').guard f g → (κ.rule zero one ρ).srcPh = (κ.rule zero one ρ').srcPh → ρ = ρ'

In-shape separation.

theorem DescriptiveComplexity.Draw.AdvKit.exit_disjoint {A Q W P : Type} [DecidableEq W] (κ : AdvKit A Q W P) (zero one : A) (hemb : Function.Injective κ.emb) (ρ : AdvRule) (f : Q → A) (g : W → A) : (κ.rule zero one ρ).guard f g → g κ.wk = one → g κ.rg ≠ one → (κ.rule zero one ρ).srcPh = κ.emb AdvPh.a4 → False

Exit disjointness at the kit's landing phase.

The discharge

theorem DescriptiveComplexity.Draw.AdvKit.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} {κ : AdvKit A Q W P} {rEmb : AdvRule → R} (hrules : ∀ (ρ : AdvRule), PR.rules (rEmb ρ) = κ.rule PR.zero PR.one ρ) {I : Type} [Finite I] {ile : I → I → Prop} (F : IxFile (Univ A R P K dd) I ile) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) (hix : IsLinOrd ile) (hnerg : κ.t ≠ κ.rg) (hnerl : κ.rl ≠ κ.t) (hnewk : κ.wk ≠ κ.t) {gtop gbot : I} (htop : ∀ (y : I), ile y gtop) (hbot : ∀ (y : I), ile gbot y) {v v' : Univ A R P K dd → Prop} (hi : WMIncr WMLe v v') (hv' : WMSetLt WMLe v' (F.cell gbot)) {m m' : I → Prop} (him : WMIncr ile m m') {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 ≠ v' → restB r = restN r) (hNwk : restN v' κ.wk = PR.zero) (hNoth : ∀ (s : W), s ≠ κ.wk → restB v' s = restN v' s) (hwkB : ∀ (r : Univ A R P K dd → Prop), restB r κ.wk = bitVal PR.zero PR.one (r = v')) (hrgB : ∀ (r : Univ A R P K dd → Prop), restB r κ.rg = bitVal PR.zero PR.one (∃ (u : I), r = F.cell u)) (hrlB : ∀ (r : Univ A R P K dd → Prop), restB r κ.rl = bitVal PR.zero PR.one (r = F.cell gtop)) {p₀ : P} {fc : Q → A} {w : ℕ} (hgap : ∀ (u u' : I), IxSucc ile u u' → wideRank (F.cell u') - wideRank (F.cell u) ≤ w) (h₀ : PR.HasRight p₀ fc (PR.passTracksAt F.cell κ.t restA m v) (κ.emb AdvPh.a1) fc (PR.passTracksAt F.cell κ.t restN m v)) : (wideData (Univ A R P K dd)).ReachesIn (wideRank (F.cell gtop) + ((ixRank ile gtop - ixRank ile gbot) * w + 1) + wideRank (F.cell gbot) + 4) { state := Sum.inr (PR.stElt p₀ fc), head := Sum.inl v, tape := wideTape (PR.trackTapeAt F.cell κ.t restA m) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (κ.emb AdvPh.a4) fc), head := Sum.inl v', tape := wideTape (PR.trackTapeAt F.cell κ.t restB m') (PR.syElt PR.blank) }

The kit advances the working cell: from the caller's phase at the old marker – whose erasing step is the caller's rule, the one hypothesis beyond the slot equations – to the kit's landing phase at the new marker, mirror incremented.

theorem DescriptiveComplexity.Draw.AdvKit.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} {κ : AdvKit A Q W P} {rEmb : AdvRule → R} (hrules : ∀ (ρ : AdvRule), PR.rules (rEmb ρ) = κ.rule PR.zero PR.one ρ) {I : Type} [Finite I] {ile : I → I → Prop} (F : IxFile (Univ A R P K dd) I ile) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) (hix : IsLinOrd ile) (hnerg : κ.t ≠ κ.rg) (hnerl : κ.rl ≠ κ.t) (hnewk : κ.wk ≠ κ.t) {gtop gbot : I} (htop : ∀ (y : I), ile y gtop) (hbot : ∀ (y : I), ile gbot y) {v v' : Univ A R P K dd → Prop} (hi : WMIncr WMLe v v') (hv' : WMSetLt WMLe v' (F.cell gbot)) {m m' : I → Prop} (him : WMIncr ile m m') {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 ≠ v' → restB r = restN r) (hNwk : restN v' κ.wk = PR.zero) (hNoth : ∀ (s : W), s ≠ κ.wk → restB v' s = restN v' s) (hwkB : ∀ (r : Univ A R P K dd → Prop), restB r κ.wk = bitVal PR.zero PR.one (r = v')) (hrgB : ∀ (r : Univ A R P K dd → Prop), restB r κ.rg = bitVal PR.zero PR.one (∃ (u : I), r = F.cell u)) (hrlB : ∀ (r : Univ A R P K dd → Prop), restB r κ.rl = bitVal PR.zero PR.one (r = F.cell gtop)) {p₀ : P} {fc : Q → A} (h₀ : PR.HasRight p₀ fc (PR.passTracksAt F.cell κ.t restA m v) (κ.emb AdvPh.a1) fc (PR.passTracksAt F.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 F.cell κ.t restA m) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (κ.emb AdvPh.a4) fc), head := Sum.inl v', tape := wideTape (PR.trackTapeAt F.cell κ.t restB m') (PR.syElt PR.blank) }

The kit runs one round of a sweep, the budget forgotten.